Abstract
The λ̄μμ̄-calculus is a variant of the λ-calculus with significant differences, including non-confluence and a Curry-Howard isomorphism with the classical sequent calculus. We present an encoding of the λ̄μμ̄-calculus into the π-calculus. We establish the operational correctness of the encoding, and then we extract from it an abstract machine for the λ̄μμ̄-calculus. We prove that there is a tight relationship between such a machine and Curien and Herbelin's abstract machine for the λ̄μμ̄-calculus. The π-calculus image of the (typed) λ̄μμ̄-calculus is a nontrivial set of terminating processes. © 2010 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Cimini, M., Coen, C. S., & Sangiorgi, D. (2010). Functions as processes: Termination and the λ̄μμ̄- calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6084 LNCS, pp. 73–86). https://doi.org/10.1007/978-3-642-15640-3_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
