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.
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
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)