Gérard Boudol
ABSTRACT
We introduce a calculus which is a direct extension of both the λ and the π calculi. We give a simple type system for it, that encompasses both Curry's type inference for the λ-calculus, and Milner's sorting for the π-calculus as particular cases of typing. We observe that the various continuation passing style transformations for λ-terms, written in our calculus, actually correspond to encodings already given by Milner and others for evaluation strategies of λ-terms into the π-calculus. Furthermore, the associated sortings correspond to well-known double negation translations on types. Finally we provide an adequate CPS transform from our calculus to the π-calculus. This shows that the latter may be regarded as an "assembly language", while our calculus seems to provide a better programming notation for higher-order concurrency.
- 1.S. ABRAMSKY, C.-H.L. ONG, FUll abstraction in the lazy lambda-calculus, Information and Computation 105 (1993) 159-267. Google Scholar
Digital Library
- 2.R. AMADIO, L. LETH, B. THOMSEN, From a concurrent A-calculus to the 7r-calculus, FCT'95, Lecture Notes in Comput. Sci. 965 (1995) 106-115. Google ScholarDigital Library
- 3.A. APPEL, Compiling with Continuations, Cambridge University Press (1992). Google ScholarDigital Library
- 4.G. BERRY, G. BOUDOL, Tile chemical abstract machine, Theoretical Comput. Sci. 96 (1992) 217-248. Google ScholarDigital Library
- 5.G. BOUDOL, Asynd#rony and the 7r-calculus, INRIA Res. Report 1702 ( 1992).Google Scholar
- 6.G. BOUDOL, The A-calculus with multiplicities, INRIA Res. Report 2025 (1993).Google Scholar
- 7.G. BOUDOL, Lambda-calculi for (strict) parallel functions, Information and Computation 108 (1994) 51-127. Google ScholarDigital Library
- 8.G. BOUDOL, C. LANEVE, A-Calculus, multiplicities and the 7r-calculus, INRIA Res. Report 2581 (1995).Google Scholar
- 9.G. BOUDOL, C. LANEVE, The discriminating power of multiplicities in the A-calculus, Information and Computation 126 (1996) 83-102. Google ScholarDigital Library
- 10.M. BOREALE, On the expressiveness of internal mobility in name-passing calculi, CONCUR'96, Lecture Notes in Comput. Sci. 1119 (1996) 163-178. Google ScholarDigital Library
- 11.C. FOURNET, G. GONTHIER, The reflexive CHAM, and the join calculus, POPL'96 (1996) 372-385. Google ScholarDigital Library
- 12.A. GIACALONE, P. MISHRA, S. PRASAD, FACILE: asymmetric integration of concurrent and functional programruing, TAPSOFT'89, Lecture Notes in Comput. Sci. 352 (#989) 184-209. Google ScholarDigital Library
- 13.R. HARPER, M. LILLIBRIDGE, Polymorphic type assignment and cPs conversion, LISP and Symbolic Computation 6 (1993) 361-380. Google ScholarDigital Library
- 14.J. LAUNCHBURY, A natural semantics for lazy evaluation, POPL'93 (1993) 144-154. Google ScholarDigital Library
- 15.A.P# MEYER, M. WAND, Continuation semantics in typed lambda-calculi, Lecture Notes in Comput. Sci. 193 (1985) 219-224. Google ScholarDigital Library
- 16.R. MILNER, J. PARROW, D. WALKER, A calculus of mobile processes, Information and Computation I00 (1992) 1-77. Google ScholarDigital Library
- 17.R. MILNER, Functions as processes, Math. Struct. in Comp. Science 2 (1992) 119-141. Preliminary version in INRIA Res. Report 1154.Google ScholarCross Ref
- 18.tL MILNER, The polyadic 7r-calculus: a tutorial, Technical Report ECS-LFCS-91-180, Edinburgh University (1991) Reprinted in Logic and Algebra of Specification, F. Bauer, W. Brauer and H. Schwichtenberg, Eds, Springer Verlag, 1993, 203-246.Google Scholar
- 19.C. MURTHY, A computational analysis of Girard's translation aJld LC, LICS'92 (1992) 90-101.Google Scholar
- 20.B. PmRCE, Programming in the #r-calculus - An experiment in concurrent language design, available electronically, Computer Lab. Cambridge (1995).Google Scholar
- 21.G. PLOTKIN, Call-by-same, call-by-value and the A-calculus, Theoret. Comput. Sci. 1 (1975) 125-159.Google ScholarCross Ref
- 22.J.H. REPPY, CML: a higher-order concurrent language, ACM SIGPLAN'91 PLDI Conference, SIGPLAN Notices 26 (1991) 293-305. Google ScholarDigital Library
- 23.D. SANGIORG{, Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms, PhD Thesis, Department of Computer Science, The University of Edinburgh (1993).Google Scholar
- 24.D. SANGIOROI, From zr-calculus to higher-order 7r-calculus- and back, TAPSOFT'93, Lecture Notes in Comput. Sci. 668 (#993) 151-166. Google ScholarDigital Library
- 25.D. SANGIORGI, The lazy lambda-calculus in a concurrency scenario, Information and Computation 120 (1994) 120-153. Google ScholarDigital Library
- 26.G. SMOLKA, A foundation for higher-order concurrent constraint programming, in Constraints in Computational Logics, Lecture Notes in Comput. Sci. 845 (1994) 50-72. Google ScholarDigital Library
- 27.C. TALCOTT, Ed., Special Issue on Continuations, LISP and Symbolic Computation 6 & 7 (1993).Google Scholar
- 28.D. TURNER, The Polymorphic Pi-calculus: Theory and h nplementation, Ph.D. Thesis, University of Edinburgh (1995).Google Scholar
- 29.V. VASCONCELOS, K. HONDA, Principal typing schemes in a polyadic 7r-calculus, CONCUR'93, Lecture Notes in Comput. Sci. 715 (1993) 524-538. Google ScholarDigital Library
Index Terms
- The π-calculus in direct style
Recommendations
The π-Calculus in Direct Style
We introduce a calculus which is a direct extension of both the λ and the π calculi. We give a simple type system for it, that encompasses both Curry‘s type inference for the λ-calculus, and Milner‘s sorting for the π-calculus as particular cases of typing. ...
Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
WoLLIC '09: Proceedings of the 16th International Workshop on Logic, Language, Information and ComputationWe give a simple intuitionistic completeness proof of Kripke semantics with constant domain for intuitionistic logic with implication and universal quantification. We use a cut-free intuitionistic sequent calculus as formal system and by combining ...
Proof systems for π-calculus logics
Logic for concurrency and synchronisationWe study the problem of verifying general temporal and functional properties of mobile and dynamic process networks, cast in terms of the π-calculus. Much of the expressive power of this calculus derives from the combination of name generation and ...
Comments