Abstract
We demonstrate a tight relationship between linearly typed π-calculi and typed λ-calculi by giving a type-preserving translation from the call-by-value λμ-calculus into a typed π-calculus. The λμ-calculus has a particularly simple representation as typed mobile processes. The target calculus is a simple variant of the linear π-calculus. We establish full abstraction up to maximally consistent observational congruences in source and target calculi using techniques from games semantics and process calculi.
Partially supported by EPSRC EP/K011715/1, EP/L00058X/1 and EP/K034413/1.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
A full version of this paper. Doc Technical Report DTR 2014/2, Department of Computing, Imperial College London (April 2014)
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full Abstraction for PCF. Info. & Comp. 163, 409–470 (2000)
Berger, M.: Program Logics for Sequential Higher-Order Control. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 194–211. Springer, Heidelberg (2010)
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)
Berger, M., Honda, K., Yoshida, N.: Genericity and the pi-calculus. Acta Inf. 42(2-3), 83–141 (2005)
Curien, P.-L., Herbelin, H.: Computing with Abstract Böhm Trees. In: Functional and Logic Programming, pp. 20–39. World Scientific (1998)
Curien, P.-L., Herbelin, H.: The duality of computation. In: Proc. ICFP, pp. 233–243 (2000)
Danvy, O., Filinski, A.: Representing control: A study of the CPS transformation. MSCS 2(4), 361–391 (1992)
de Groote, P.: On the Relation between the lambda-mu-calculus and the Syntactic Theory of Sequential Control. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol. 822, pp. 31–43. Springer, Heidelberg (1994)
Felleisen, M., Friedman, D.P., Kohlbecker, E., Duba, B.: Syntactic theories of sequential control. TCS 52, 205–237 (1987)
Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. TCS 103(2), 235–271 (1992)
Führmann, C., Thielecke, H.: On the call-by-value CPS transform and its semantics. Inf. Comput. 188(2), 241–283 (2004)
Griffin, T.G.: A formulae-as-type notion of control. In: Proc. POPL, pp. 47–58 (1990)
Honda, K., Laurent, O.: An exact correspondence between a typed pi-calculus and polarised proof-nets. Theor. Comput. Sci. 411(22-24), 2223–2238 (2010)
Honda, K., Yoshida, N.: On reduction-based process semantics. TCS 151, 393–456 (1995)
Honda, K., Yoshida, N.: Game-theoretic analysis of call-by-value computation. TCS 221, 393–456 (1999)
Honda, K., Yoshida, N.: Noninterference through flow analysis. JFP 15(2), 293–349 (2005)
Honda, K., Yoshida, N.: A uniform type structure for secure information flow. TOPLAS 29(6) (2007)
Hyland, J.M.E., Ong, C.H.L.: On full abstraction for PCF. Inf. & Comp. 163, 285–408 (2000)
Laird, J.: A semantic analysis of control. PhD thesis, University of Edinburgh (1998)
Laird, J.: A game semantics of linearly used continuations. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 313–327. Springer, Heidelberg (2003)
Laurent, O.: Polarized games. In: Proc. LICS, pp. 265–274 (2002)
Laurent, O.: Polarized proof-nets and λμ-calculus. TCS 290(1), 161–188 (2003)
Milner, R.: Functions as Processes. MSCS 2(2), 119–141 (1992)
Moggi, E.: Notions of computation and monads. Inf. & Comp. 93(1), 55–92 (1991)
Ong, C.-H.L., Stewart, C.A.: A Curry-Howard foundation for functional computation with control. In: Proc. POPL, pp. 215–227 (1997)
Parigot, M.: λ-μ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)
Reynolds, J.: The discovers of continuations. Lisp and Symbolic Computation 6, 233–247 (1993)
Robinson, E.: Kohei Honda. Bulletin of the EATCS 112 (February 2014)
Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. In: Proc. LFP, pp. 288–298 (1992)
Sangiorgi, D.: π-calculus, internal mobility and agent-passing calculi. TCS 167(2), 235–274 (1996)
Sangiorgi, D.: From λ to π: or, rediscovering continuations. MSCS 9, 367–401 (1999)
Sassone, V.: ETAPS Award: Laudatio for Kohei Honda. Bulletin of the EATCS 112 (February 2014)
Selinger, P.: Control categories and duality: on the categorical semantics of the lambda-mu calculus. MSCS 11(2), 207–260 (2001)
Thielecke, H.: Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh (1997)
Thielecke, H.: Continuations, functions and jumps. SIGACT News 30(2), 33–42 (1999)
van Bakel, S., Vigliotti, M.G.: An Output-Based Semantics of Λμ with Explicit Substitution in the π-Calculus. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 372–387. Springer, Heidelberg (2012)
Wadler, P.: Call-by-value is dual to call-by-name. In: Proc. ICFP, pp. 189–201 (2003)
Yoshida, N., Berger, M., Honda, K.: Strong normalisation in the π-calculus. Inf. Comput. 191(2), 145–202 (2004)
Yoshida, N., Honda, K., Berger, M.: Linearity and bisimulation. J. Log. Algebr. Program. 72(2), 207–238 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Honda, K., Yoshida, N., Berger, M. (2014). Process Types as a Descriptive Tool for Interaction. In: Dowek, G. (eds) Rewriting and Typed Lambda Calculi. RTA TLCA 2014 2014. Lecture Notes in Computer Science, vol 8560. Springer, Cham. https://doi.org/10.1007/978-3-319-08918-8_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-08918-8_1
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08917-1
Online ISBN: 978-3-319-08918-8
eBook Packages: Computer ScienceComputer Science (R0)