Abstract
We investigate a notion of behavioral genericity in the context of session type disciplines. To this end, we develop a logically motivated theory of parametric polymorphism, reminiscent of the Girard-Reynolds polymorphic λ-calculus, but casted in the setting of concurrent processes. In our theory, polymorphism accounts for the exchange of abstract communication protocols and dynamic instantiation of heterogeneous interfaces, as opposed to the exchange of data types and dynamic instantiation of individual message types. Our polymorphic session-typed process language satisfies strong forms of type preservation and global progress, is strongly normalizing, and enjoys a relational parametricity principle. Combined, our results confer strong correctness guarantees for communicating systems. In particular, parametricity is key to derive non-trivial results about internal protocol independence, a concurrent analogous of representation independence, and non-interference properties of modular, distributed systems.
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
Berger, M., Honda, K., Yoshida, N.: Genericity and the π-Calculus. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 103–119. Springer, Heidelberg (2003)
Berger, M., Honda, K., Yoshida, N.: Genericity and the pi-calculus. Acta Inf. 42(2-3), 83–141 (2005)
Bono, V., Padovani, L.: Polymorphic endpoint types for copyless message passing. In: Proc. of ICE 2011. EPTCS, vol. 59, pp. 52–67 (2011)
Bono, V., Padovani, L.: Typing copyless message passing. Logical Methods in Computer Science 8(1) (2012)
Caires, L., Pérez, J.A., Pfenning, F., Toninho, B.: Relational parametricity for polymorphic session types. Tech. rep., CMU-CS-12-108, Carnegie Mellon Univ. (April 2012)
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)
Caires, L., Pfenning, F., Toninho, B.: Linear logic propositions as session types (2012), under Revision - http://www.cs.cmu.edu/~fp/papers/sessions12.pdf
Caires, L., Pfenning, F., Toninho, B.: Towards concurrent type theory. In: TLDI 2012, pp. 1–12. ACM, New York (2012)
Dardha, O., Giachino, E., Sangiorgi, D.: Session Types Revisited. In: PPDP, pp. 139–150. ACM (2012)
Dezani-Ciancaglini, M., Giachino, E., Drossopoulou, S., Yoshida, N.: Bounded Session Types for Object Oriented Languages. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol. 4709, pp. 207–245. Springer, Heidelberg (2007)
Gay, S., Hole, M.: Subtyping for session types in the pi calculus. Acta Inf. 42, 191–225 (2005)
Gay, S.J.: Bounded polymorphism in session types. Math. Struc. in Comp. Sci. 18(5), 895–930 (2008)
Girard, J.Y.: Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination de coupures dans l’analyse et la théorie des types. In: Proc. of the 2nd Scandinavian Logic Symposium, pp. 63–92. North-Holland Publishing Co. (1971)
Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1989)
Goto, M., Jagadeesan, R., Jeffrey, A., Pitcher, C., Riely, J.: An Extensible Approach to Session Polymorphism (2012), http://fpl.cs.depaul.edu/projects/xpol/
Harper, R.: Practical Foundations for Programming Languages. Cambridge University Press (2012)
Honda, K.: Types for Dyadic Interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993)
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)
Jeffrey, A., Rathke, J.: Full abstraction for polymorphic pi-calculus. Theor. Comput. Sci. 390(2-3), 171–196 (2008)
Pérez, J.A., Caires, L., Pfenning, F., Toninho, B.: Linear Logical Relations for Session-Based Concurrency. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 539–558. Springer, Heidelberg (2012)
Pfenning, F., Caires, L., Toninho, B.: Proof-Carrying Code in a Session-Typed Process Calculus. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 21–36. Springer, Heidelberg (2011)
Pierce, B.C., Sangiorgi, D.: Behavioral equivalence in the polymorphic pi-calculus. J. ACM 47(3), 531–584 (2000)
Reynolds, J.C.: Towards a theory of type structure. In: Programming Symposium, Proceedings Colloque sur la Programmation, pp. 408–423. Springer, London (1974)
Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Mason, R.E.A. (ed.) Information Processing 1983, pp. 513–523. Elsevier Science Publishers B. V. (1983)
Sangiorgi, D., Walker, D.: The π-calculus: A Theory of Mobile Processes. Cambridge University Press, New York (2001)
Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: Proc. of PPDP 2011, pp. 161–172. ACM, New York (2011)
Turner, D.: The polymorphic pi-calculus: Theory and implementation. Tech. rep., ECS-LFCS-96-345, Univ. of Edinburgh (1996)
Wadler, P.: Propositions as sessions. In: Thiemann, P., Findler, R.B. (eds.) ICFP, pp. 273–286. ACM (2012)
Washburn, G., Weirich, S.: Generalizing parametricity using information-flow. In: LICS, pp. 62–71. IEEE Computer Society (2005)
Zhao, J., Zhang, Q., Zdancewic, S.: Relational Parametricity for a Polymorphic Linear Lambda Calculus. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 344–359. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Caires, L., Pérez, J.A., Pfenning, F., Toninho, B. (2013). Behavioral Polymorphism and Parametricity in Session-Based Communication. In: Felleisen, M., Gardner, P. (eds) Programming Languages and Systems. ESOP 2013. Lecture Notes in Computer Science, vol 7792. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37036-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-37036-6_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37035-9
Online ISBN: 978-3-642-37036-6
eBook Packages: Computer ScienceComputer Science (R0)