B. Thomsen
ABSTRACT
In this paper we present A Calculus of Higher Order Communicating Systems. This calculus considers sending and receiving processes to be as fundamental as nondeterminism and parallel composition.
The calculus is an extension of CCS [Mil80] in the sense that all the constructions of CCS are included or may be derived from more fundamental constructs and most of the mathematical framework of CCS carries over almost unchanged.
Clearly CCS with processes as first class objects is a powerful metalanguage and we show that it is possible to simulate the untyped λ-calculus in CHOCS. The relationship between CHOCS and the untyped λ-calculus is further strengthened by a result showing that the recursion operator is unnecessary in the sense that recursion can be simulated by means of process passing and communication.
As pointed out by R. Milner in [Mil80], CCS has its limitations when one wants to describe unboundedly expanding systems as e.g. an unbounded number of procedure invocations in an imperative concurrent programming language. We show how neatly CHOCS may describe both call by value and call by reference parameter mechanisms for the toy language of chapter 6 in [Mil80].
- Abr87a.S. Abramsky: Domain Theory in Logical Form, Proceedings of LICS 87. Full version submitted to AnnMs of Pure and Applied Logic, 1987.Google Scholar
- Abr87b.S. Abr~msky: A Domain Equation For Bisimulation, Unpublished manuscript, Dept. Computing, Imperial College, London 1987.Google Scholar
- Abr88.S. Abr~msky: The Lazy Lambda Calculus, to appear in Declarative Prg. ed. D. Turner, Addison Wesley, 1988.Google Scholar
- AusBou84.D. Austry & G. Boudol: Alg~bre de Processus et Synchronisatiou, Theoretical Computer Science 30(1) pp. 91-131, 1984.Google ScholarCross Ref
- AstReg87.E. Astesiano & G. Reggio: SMoLS-Driven Concurrent Calculi, Proceeding from TAPSOFT 87, Pisa, LNCS 249, Springer Verlag, 1987. Google ScholarDigital Library
- Bar85.H.P. Barendreght: The Lambda Calculus -- Its Syntaz and Semantics, North-Holland 1985.Google Scholar
- BerKlo84.j. Bergstra & J. W. Klop: Process Algebra for Synchronous Communication, Information and Control 60, pp. 109-137, 1984.Google ScholarCross Ref
- Bou88.G. Boudol: Towards a Lambda-Calculus for Concurrent and Communicating Systems~ Research Report hr. 885, INRIA Sophia Antipolis, Autumn 1988.Google Scholar
- Chr88.P. Christen~en: The Domain of CSP Proce~se~, incomplete draft, The Technical University of Denmark, 1988.Google Scholar
- CouCou79.P. Cousot & R. Cousot: Systematic design of Program Analysis Frameworks, In: Conf. Record of the 6th ACM symposium on Principles of Programming Lattguages 1979. Google ScholarDigital Library
- dNiHen87.M. Hennessy & R. de Nicola: CCS without r 's, Proceeding from TAPSOFT 87, Pisa, LNCS 249, Springer Verlag, 1987. Google ScholarDigital Library
- EngNie86.U. Engberg & M. Nielsen: A Calculus of Communicating Systems with Label Passing, DAIMI PB-208 Aarhus University Computer Science Department, 1986.Google Scholar
- HenMil85.M. Hennessy &." R. Milner: Algebraic Laws for Nondeterminism and Concurrency, Journal of the Association for Computing Machinery, pp. 137-161, 1985. Google ScholarDigital Library
- KenSle83.J. P~. Kennaway & M. R. Sleep: Syntax and Informal Semantics of DyNe, a Parallel language, LNCS 207, Springer Verlag, 1983. Google ScholarDigital Library
- KenSle88.J. R. Kennaway & M. R. Sleep: A Denotational Semantics for First Class Processes, Draft, School of Information Systems, University of East Anglia, Norwich, U.K., August 1988.Google Scholar
- Mil80.R. Milner: A Calculus of Communicating Systems, LNCS 92.. Springer Verlag, 1980. Google ScholarDigital Library
- Mil81.R. Milner: A Complete Inference System for a Class of Regular Behaviours, University of Edinburgh 1981.Google Scholar
- Mil83.R. Milner: Calculi for Synchrony and Asynchrony, Theoretical Computer Science 25 (1983), pp 269-310, North Holland.Google Scholar
- Mil83b.K. Mihter: Parallel Combinator Reduction Machine, LNCS 207, Springer Verlag, 1983.Google Scholar
- Nie88.F. Nielson: The Typed .~-Calculus with First- Class Processe,~, Technical Report ID-TR: 1988- 43 ISSN 0902-2821, Department of Computer Science, Technical University of Denmark, August 1988.Google Scholar
- Par81.D. Park: Concurrency and Automata on Infinite Sequences, LNCS 104, Springer Verlag, 1981. Google ScholarDigital Library
- Plo81.G. Plotkin: A Structural Approach to Operational Semantics, DAIMI FN-19 Aarhus University Computer Science Department 1981.Google Scholar
- Pra88.K.V.S. Prasad: Combinators and Bisimulation Proofs for Restartable Systems, Ph. D Thesis, Edinburgh University, 1988. Google ScholarDigital Library
- Tar55.A. Tarski: A Lattice-Theoretical Fixpoint Theorem and Its Applications, Pacific Journal of Math. 5, 1955.Google Scholar
- Wal88.D. Walker: Bi~simulation and Divergence, Proc. of LICS 88, ISBN 0-8186-0853-6.Google Scholar
Index Terms
- A calculus of higher order communicating systems
Recommendations
Expressing first-order π-calculus in higher-order calculus of communicating systems
In the study of process calculi, encoding between different calculi is an effective way to compare the expressive power of calculi and can shed light on the essence of where the difference lies. Thomsen and Sangiorgi have worked on the higher-order ...
Higher-order abstract syntax in classical higher-order logic
LFMTP '09: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and PracticeHigher-Order Abstract Syntax, or HOAS, is a technique for using a higher-order logic as a metalanguage for an object language with binding operators. It avoids formalizing syntactic details related to variable binding. This paper gives an extension to ...
Formalization of the Resolution Calculus for First-Order Logic
I present a formalization in Isabelle/HOL of the resolution calculus for first-order logic with formal soundness and completeness proofs. To prove the calculus sound, I use the substitution lemma, and to prove it complete, I use Herbrand interpretations ...
Comments