Abstract
We study type-directed encodings of the simply-typed λ-calculus in a session-typed π-calculus. The translations proceed in two steps: standard embeddings of simply-typed λ-calculus in a linear λ-calculus, followed by a standard translation of linear natural deduction to linear sequent calculus. We have shown in prior work how to give a Curry-Howard interpretation of the proofs in the linear sequent calculus as π-calculus processes subject to a session type discipline. We show that the resulting translations induce sharing and copying parallel evaluation strategies for the original λ-terms, thereby providing a new logically motivated explanation for these strategies.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Barber, A., Plotkin, G.: Dual Intuitionistic Linear Logic. Technical Report LFCS-96-347. Univ. of Edinburgh (1997)
Beffara, E.: Functions as proofs as processes. CoRR, abs/1107.4160 (2011)
Berger, M., Honda, K., Yoshida, N.: Sequentiality and the π-Calculus. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 29–45. Springer, Heidelberg (2001)
Boreale, M.: On the Expressiveness of Internal Mobility in Name-Passing Calculi. Theoretical Computer Science 195(2), 205–226 (1998)
Boudol, G.: The lambda-calculus with multiplicities. Technical report, INRIA (1993)
Caires, L., Pfenning, F.: Session Types as Intuitionistic Linear Propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 222–236. Springer, Heidelberg (2010)
Faggian, C., Piccolo, M.: Ludics is a Model for the Finitary Linear pi-Calculus. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 148–162. Springer, Heidelberg (2007)
Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)
Gonthier, G., Abadi, M., Lévy, J.-J.: The geometry of optimal lambda reduction. In: POPL 1992, Proceedings the Nineteenth Annual ACM Symposium on Principles of Programming Languages, pp. 15–26 (1992)
Halstead Jr., R.H.: Multilisp: a language for concurrent symbolic computation. ACM Trans. Program. Lang. Syst. 7, 501–538 (1985)
Honda, K., Laurent, O.: An exact correspondence between a typed pi-calculus and polarised proof-nets. Theor. Comp. Sci. 411, 2223–2238 (2010)
Honda, K., Vasconcelos, V.T., Kubo, M.: Language Primitives and Type Discipline for Structured Communication-Based Programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)
Lafont, Y.: Interaction nets. In: POPL 1990, pp. 95–108. ACM, New York (1990)
Lamping, J.: An algorithm for optimal lambda calculus reduction. In: POPL 1990, Proceedings the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pp. 16–30 (1990)
Maraist, J., Odersky, M., Turner, D.N., Wadler, P.: Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Electr. Notes Theor. Comput. Sci. 1, 370–392 (1995)
Mazza, D.: Multiport Interaction Nets and Concurrency. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 21–35. Springer, Heidelberg (2005)
Milner, R.: Functions as processes. Math. Struct. in Comp. Sci. 2(2), 119–141 (1992)
Sangiorgi, D.: Pi-Calculus, Internal Mobility, and Agent Passing Calculi. Theoretical Computer Science 167(1&2), 235–274 (1996)
Sangiorgi, D., Walker, D.: The π-calculus: A Theory of Mobile Processes. Cambridge University Press (2001)
Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: PPDP 2011, pp. 161–172. ACM (2011)
van Bakel, S., Vigliotti, M.G.: A Logical Interpretation of the Λ-Calculus into the π-Calculus. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 84–98. Springer, Heidelberg (2009)
Wadler, P.: A Syntax for Linear Logic. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 513–529. Springer, Heidelberg (1994)
Wadsworth, C.: Semantics and Pragmatics of the Lambda Calculus. PhD thesis, Oxford University (1971)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Toninho, B., Caires, L., Pfenning, F. (2012). Functions as Session-Typed Processes. In: Birkedal, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2012. Lecture Notes in Computer Science, vol 7213. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28729-9_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-28729-9_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28728-2
Online ISBN: 978-3-642-28729-9
eBook Packages: Computer ScienceComputer Science (R0)