ABSTRACT
Session types describe structured communication on heterogeneously typed channels at a high level. Their tail-recursive structure imposes a protocol that can be described by a regular language. The types of transmitted values are drawn from the underlying functional language, abstracting from the details of serializing values of structured data types.
Context-free session types extend session types by allowing nested protocols that are not restricted to tail recursion. Nested protocols correspond to deterministic context-free languages. Such protocols are interesting in their own right, but they are particularly suited to describe the low-level serialization of tree-structured data in a type-safe way.
We establish the metatheory of context-free session types, prove that they properly generalize standard (two-party) session types, and take first steps towards type checking by showing that type equivalence is decidable.
- L. Aceto and M. Hennessy. Termination, deadlock, and divergence. J. ACM, 39(1):147–187, 1992. Google ScholarDigital Library
- J. C. M. Baeten, J. A. Bergstra, and J. W. Klop. Decidability of bisimulation equivalence for processes generating context-free languages. J. ACM, 40(3):653–682, 1993. Google ScholarDigital Library
- G. Bernardi and M. Hennessy. Using higher-order contracts to model session types. Logical Methods in Computer Science, 12(2:10):1–43, 2016.Google Scholar
- V. Bono, L. Padovani, and A. Tosatto. Polymorphic types for leak detection in a session-oriented functional language. In FORTE, volume 7892 of LNCS, pages 83–98. Springer, 2013.Google Scholar
- L. Caires and F. Pfenning. Session types as intuitionistic linear propositions. In CONCUR, volume 6269 of LNCS, pages 222–236. Springer, 2010. Google ScholarDigital Library
- M. Carbone, K. Honda, and N. Yoshida. Structured communicationcentered programming for web services. ACM Trans. Program. Lang. Syst., 34(2):8, 2012. Google ScholarDigital Library
- S. Christensen, H. Hüttel, and C. Stirling. Bisimulation equivalence is decidable for all context-free processes. Inf. Comput., 121(2):143– 148, 1995. Google ScholarDigital Library
- B. Courcelle. Fundamental properties of infinite trees. Theoretical Comput. Sci., 25:95–169, 1983.Google ScholarCross Ref
- S. J. Gay. Bounded polymorphism in session types. Mathematical Structures in Computer Science, 18(5):895–930, 2008.Google ScholarCross Ref
- S. J. Gay and M. Hole. Subtyping for session types in the pi calculus. Acta Informaticæ, 42(2-3):191–225, 2005.Google ScholarDigital Library
- S. J. Gay and V. T. Vasconcelos. Linear type theory for asynchronous session types. J. Funct. Program., 20(1):19–50, 2010. Google ScholarDigital Library
- S. J. Gay, V. T. Vasconcelos, A. Ravara, N. Gesbert, and A. Z. Caldeira. Modular session types for distributed object-oriented programming. In POPL, pages 299–312. ACM, 2010. Google ScholarDigital Library
- K. Honda. Types for dyadic interaction. In CONCUR, volume 715 of LNCS, pages 509–523. Springer, 1993. Google ScholarDigital Library
- K. Honda, V. T. Vasconcelos, and M. Kubo. Language primitives and type discipline for structured communication-based programming. In ESOP, volume 1381 of LNCS, pages 122–138. Springer, 1998. Google ScholarDigital Library
- K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In POPL, pages 273–284. ACM, 2008. Google ScholarDigital Library
- H. Hüttel, I. Lanese, V. T. Vasconcelos, L. Caires, M. Carbone, P.-M. Deniélou, D. Mostrous, L. Padovani, A. Ravara, E. Tuosto, H. T. Vieira, and G. Zavattaro. Foundations of session types and behavioural contracts. ACM Comput. Surv., 49(1), 2016. Google ScholarDigital Library
- I. Lanese, J. A. Pérez, D. Sangiorgi, and A. Schmitt. On the expressiveness and decidability of higher-order process calculi. Inf. Comput., 209(2):198–226, 2011. Google ScholarDigital Library
- B. C. Pierce. Types and Programming Languages. MIT Press, 2002. Google ScholarDigital Library
- J. H. Reppy. CML: A higher-order concurrent language. In PLDI, pages 293–305. ACM, 1991. Google ScholarDigital Library
- D. Sangiorgi. An Introduction to Bisimulation and Coinduction. Cambridge University Press, 2014. ISBN 9781139161381. Google ScholarDigital Library
- K. Takeuchi, K. Honda, and M. Kubo. An interaction-based language and its typing system. In PARLE, volume 817 of LNCS, pages 398– 413. Springer, 1994. Google ScholarDigital Library
- B. Toninho, L. Caires, and F. Pfenning. Higher-order processes, functions, and sessions: A monadic integration. In ESOP, volume 7792 of LNCS, pages 350–369. Springer, 2013. Google ScholarDigital Library
- P. Wadler. Propositions as sessions. J. Funct. Program., 24(2-3):384– 418, 2014.Google ScholarCross Ref
- D. Walker. Advanced Topics in Types and Programming Languages, chapter Substructural Type Systems. MIT Press, 2005.Google Scholar
Index Terms
Context-free session types
Recommendations
Label-dependent session types
Session types have emerged as a typing discipline for communication protocols. Existing calculi with session types come equipped with many different primitives that combine communication with the introduction or elimination of the transmitted value.
...
Context-free session types
ICFP '16Session types describe structured communication on heterogeneously typed channels at a high level. Their tail-recursive structure imposes a protocol that can be described by a regular language. The types of transmitted values are drawn from the ...
Gradual session types
Session types are a rich type discipline, based on linear types, that lift the sort of safety claims that come with type systems to communications. However, web-based applications and micro services are often written in a mix of languages, with type ...
Comments