Abstract
We explore the (dynamic) semantics of a simply typed λ-calculus enriched with parallel composition, dynamic channel generation, and input-output communication primitives. The calculus, called the λ∥-calculus, can be regarded as the kernel of concurrent-functional languages such as LCS, CML and Facile, and it can be taken as a basis for the definition of abstract machines, the transformation of programs, and the development of modal specification languages. The main technical contribution of this paper is the proof of adequacy of a compact translation of the λ ∥-calculus into the π-calculus.
This work is partially supported by ESPRIT BRA 6454 Confer.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
R. Amadio. Translating Core Facile. Technical Report ECRC-94-3, ECRC, Munich, 1994.
R. Amadio, L. Leth, and B. Thomsen. From a Concurrent λ-calculus to the π-calculus. Technical Report ECRC-95-18, ECRC, Munich, 1995.
D. Berry, R. Milner, and D. N. Turner. A semantics for ML concurrency primitives. In Proceedings of POPL'92. ACM, 1992.
B. Berthomieu, D. Giralt, and J-P. Gouyon. Lcs users' manual. Technical report 91226, LAAS/CNRS, 1991.
A. Giacalone, P. Mishra, and S. Prasad. Facile: A symmetric integration of concurrent and functional programming. International Journal of Parallel Programming, 18(2):121–160, 1989.
A. Giacalone, P. Mishra, and S. Prasad. Operational and algebraic semantics for facile: A symmetric integration of concurrent and functional programming. In Proceedings of ICALP 90, LNCS 443. Springer-Verlag, 1990.
R. Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119–141, 1992.
R. Milner. The polyadic π-calculus: A tutorial. In W. Brauer F.L. Bauer and H. Schwichtenberg, editors, Logic and Algebra of Specification. Springer-Verlag, 1993.
R. Milner, J. Parrow, and D. Walker. A Calculus of Mobile Process, Parts 1–2. Information and Computation, 100(1):1–77, 1992.
R. Milner and D. Sangiorgi. Barbed bisimulation. In SLNCS 623: Proceedings of ICALP 92. Springer-Verlag, 1992.
J. Reppy. Cml: A higher-order concurrent language. In Proc. ACM-SIGPLAN 91, Conf. on Prog. Lang. Design and Impl., 1991.
B. Thomsen. Plain chocs. Acta Informatica, 30:1–59, 1993. Also appeared as TR 89/4, Imperial College, London.
B. Thomsen, L. Leth, and A. Giacalone. Some issues in the semantics of facile distributed programming. In SLNCS 666: Proceedings of REX School. Springer-Verlag, 1992. Also appeared as Tech Report ECRC 92-32.
B. Thomsen, L. Leth, S. Prasad, T.M. Kuo, A. Kramer, F. Knabe, and A. Giacalone. Facile antigua release programming guide. Technical Report ECRC-93-20, ECRC, Munich, December 1993.
Victor, B. and Moller, F. The Mobility Workbench — A Tool for the π-Calculus. In Proceedings of the 6th International Conference on Computer Aided Verification, CAV'94, volume 818 of SLNCS, pages 428–440. Springer-Verlag, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amadio, R.M., Leth, L., Thomsen, B. (1995). From a concurrent λ-calculus to the π-calculus. In: Reichel, H. (eds) Fundamentals of Computation Theory. FCT 1995. Lecture Notes in Computer Science, vol 965. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60249-6_43
Download citation
DOI: https://doi.org/10.1007/3-540-60249-6_43
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60249-1
Online ISBN: 978-3-540-44770-2
eBook Packages: Springer Book Archive