Abstract
We introduce a concise pi-calculus with directed choices and develop a theory of subtyping. Built on a simple behavioural intuition, the calculus offers exact semantic analysis of the extant notions of subtyping in functional programming languages and session-based programming languages. After illustrating the idea of subtyping through examples, we show type-directed embeddings of two known subtyped calculi, one for functions and another for session-based communications. In both cases, the behavioural content of the original subtyping is precisely captured in the fine-grained subtyping theory in the pi-calculus. We then establish full abstraction of these embeddings with respect to their standard semantics, Morris’s contextual congruence in the case of the functional calculus and testing equivalence for the concurrent calculus. For the full abstraction of the embedding of the session-based calculus, we introduce a new proof method centring on non-deterministic computational adequacy and definability. Partially suggested by a technique used by Quaglia and Walker for their full abstraction result, the new proof method extends the framework used in game-based semantics to the May/Must equivalences, giving a uniform proof method for both deterministic and non-deterministic languages.
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., Cardelli, L.: A semantics of object types. In: LICS, pp. 332–341. IEEE Computer Society, Los Alamitos (1994)
Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM Trans. Program. Lang. Syst. 15(4), 575–631 (1993)
Berger, M., Honda, K., Yoshida, N.: Genericity and the pi-calculus. Acta. Inf. 42(2-3), 83–141 (2005)
Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. ACM Comput. Surv. 17(4), 471–522 (1985)
Castagna, G., Nicola, R.D., Varacca, D.: Semantic subtyping for the pi-calculus. Theor. Comput. Sci. 398, 217–242 (2008)
Castellani, I., Hennessy, M.: Testing theories for asynchronous languages. In: Arvind, V., Ramanujam, R., (eds.) FST TCS 1998. LNCS, vol. 1530, pp. 90–102. Springer, Heidelberg (1998)
Demangeon, R., Honda, K.: Full abstraction in a subtyped pi-calculus with linear types, long version (2011) (in preparation), http://perso.ens-lyon.fr/romain.demangeon/subtyping_long.pdf
Dezani-Ciancaglini, M., de’Liguoro, U.: Sessions and Session Types: An Overview. In: Laneve, C., Su, J. (eds.) WS-FM 2009. LNCS, vol. 6194, pp. 1–28. Springer, Heidelberg (2010)
Fiore, M.P., Honda, K.: Recursive types in games: Axiomatics and process representation. In: LICS, pp. 345–356 (1998)
Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta. Inf. 42(2-3), 191–225 (2005)
Honda, K.: Composing processes. In: POPL, pp. 344–357 (1996)
Honda, K.: Processes and games. Electr. Notes Theor. Comput. Sci. 71 (2002)
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)
Honda, K., Yoshida, N.: Game-theoretic analysis of call-by-value computation. Theor. Comput. Sci. 221(1-2), 393–456 (1999)
Laird, J.: A game semantics of the asynchronous pi-calculus. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 51–65. Springer, Heidelberg (2005)
Milner, R.: Functions as processes. Mathematical Structures in Computer Science 2(2), 119–141 (1992)
Morris, J.H.: Lambda-Calculus Models of Programming Languages. PhD Thesis, M.I.T (1968)
Padovani, L.: Session types at the mirror. In: ICE, pp. 71–86 (2009)
Padovani, L.: Fair subtyping for multi-party session types. In: De Meuter, W., Roman, G.-C. (eds.) COORDINATION 2011. LNCS, vol. 6721, pp. 127–141. Springer, Heidelberg (2011)
Pierce, B.C.: Types and programming languages. MIT Press, Cambridge (2002)
Pierce, B.C., Sangiorgi, D.: Typing and subtyping for mobile processes. Mathematical Structures in Computer Science 6(5), 409–453 (1996)
Pierce, B.C., Steffen, M.: Higher-order subtyping. Theor. Comput. Sci. 176(1-2), 235–282 (1997)
Quaglia, P., Walker, D.: Types and full abstraction for polyadic pi-calculus. Inf. Comput. 200(2), 215–246 (2005)
Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: Halatsis, C., Philokyprou, G., Maritsas, D., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398–413. Springer, Heidelberg (1994)
Turner, N.: The polymorphic pi-calculus: Theory and Implementation. PhD thesis, Department of Computer Science, University of Edinburgh (1996)
Walker, D.: Objects in the pi-calculus. Inf. Comput. 116(2), 253–271 (1995)
Yoshida, N., Berger, M., Honda, K.: Strong Normalisation in the Pi-Calculus. Information and Computation 191(2), 145–202 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Demangeon, R., Honda, K. (2011). Full Abstraction in a Subtyped pi-Calculus with Linear Types. In: Katoen, JP., König, B. (eds) CONCUR 2011 – Concurrency Theory. CONCUR 2011. Lecture Notes in Computer Science, vol 6901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23217-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-23217-6_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-23216-9
Online ISBN: 978-3-642-23217-6
eBook Packages: Computer ScienceComputer Science (R0)