Abstract
We define a new, output-based encoding of the λ-calculus into the asynchronous π-calculus – enriched with pairing – that has its origin in mathematical logic, and show that this encoding respects one-step spine-reduction up to substitution, and that normal substitution is respected up to similarity. We will also show that it fully encodes lazy reduction of closed terms, in that term-substitution as well as each reduction step are modelled up to similarity. We then define a notion of type assignment for the π-calculus that uses the type constructor →, and show that all Curry-assignable types are preserved by the encoding.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Gordon, A.: A Calculus for Cryptographic Protocols: The Spi Calculus. In: CC&CS 1997, pp. 36–47 (1997)
Abramsky, S.: The lazy lambda calculus. In: Research topics in functional programming, pp. 65–116 (1990)
Abramsky, S.: Proofs as Processes. TCS 135(1), 5–9 (1994)
van Bakel, S., Cardelli, L., Vigliotti, M.G.: From X to π; Representing the Classical Sequent Calculus in π-calculus. In: CL&C 2008 (2008)
van Bakel, S., Lengrand, S., Lescanne, P.: The language formula_image: Circuits, computations and classical logic. In: Coppo, M., Lodi, E., Pinna, G.M. (eds.) ICTCS 2005. LNCS, vol. 3701, pp. 81–96. Springer, Heidelberg (2005)
van Bakel, S., Lescanne, P.: Computation with Classical Sequents. MSCS 18, 555–609 (2008)
Barendregt, H.: The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam (1984)
Barendregt, H.P., Kennaway, R., Klop, J.W., Sleep, M.R.: Needed Reduction and Spine Strategies for the Lambda Calculus. I&C 75(3), 191–231 (1987)
Bellin, G., Scott, P.J.: On the pi-Calculus and Linear Logic. TCS 135(1), 11–65 (1994)
Bloo, R., Rose, K.H.: Preservation of Strong Normalisation in Named Lambda Calculi with Explicit Substitution and Garbage Collection. In: CSN 1995 – Computer Science in the Netherlands, pp. 62–72 (1995)
Church, A.: A note on the entscheidungsproblem. JSL 1(1), 40–41 (1936)
Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, p. 68, 1935. North Holland, Amsterdam (1969)
Gentzen, G.: Untersuchungen über das Logische Schliessen. Mathematische Zeitschrift 39, 176–210, 405–431 (1935)
Goubault-Larrecq, J.: A Few Remarks on SKInT. RR-3475, INRIA Rocquencourt (1998)
Honda, K., Tokoro, M.: An object calculus for asynchronous communication. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 133–147. Springer, Heidelberg (1991)
Honda, K., Yoshida, N.: On the Reduction-based Process Semantics. TCS 151, 437–486 (1995)
Honda, K., Yoshida, N., Berger, M.: Control in the π-Calculus. In: CW 2004 (2004)
Milner, R.: Function as processes. MSCS 2(2), 269–310 (1992)
Parigot, M.: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)
Sangiorgi, D.: Expressing Mobility in Process Algebra: First Order and Higher order Paradigms. PhD thesis, Edinburgh University (1992)
Sangiorgi, D.: An Investigation into Functions as Processes. In: Main, M.G., Melton, A.C., Mislove, M.W., Schmidt, D., Brookes, S.D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 143–159. Springer, Heidelberg (1994)
Sangiorgi, D.: Lazy functions and processes. RR2515, INRIA, Sophia-Antipolis (1995)
Sangiorgi, D., Walker, D.: The Pi-Calculus. Cambridge University Press, Cambridge (2003)
Sestoft, P.: Standard ML on the Web server. Department of Mathematics and Physics, Royal Veterinary and Agricultural University, Denmark (1996)
Thielecke, H.: Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh (1997)
Urban, C.: Classical Logic and Computation. PhD thesis, University of Cambridge (2000)
Urban, C., Bierman, G.M.: Strong normalisation of cut-elimination in classical logic. FI 45(1, 2), 123–155 (2001)
de Vries, F.-J.: Böhm trees, bisimulations and observations in lambda calculus. In: FLP 1997, pp. 230–245 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Bakel, S., Vigliotti, M.G. (2009). A Logical Interpretation of the λ-Calculus into the π-Calculus, Preserving Spine Reduction and Types. In: Bravetti, M., Zavattaro, G. (eds) CONCUR 2009 - Concurrency Theory. CONCUR 2009. Lecture Notes in Computer Science, vol 5710. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04081-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-04081-8_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04080-1
Online ISBN: 978-3-642-04081-8
eBook Packages: Computer ScienceComputer Science (R0)