skip to main content
10.1145/2951913.2951926acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
research-article

Context-free session types

Published:04 September 2016Publication History

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.

References

  1. L. Aceto and M. Hennessy. Termination, deadlock, and divergence. J. ACM, 39(1):147–187, 1992. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  3. 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 ScholarGoogle Scholar
  4. 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 ScholarGoogle Scholar
  5. L. Caires and F. Pfenning. Session types as intuitionistic linear propositions. In CONCUR, volume 6269 of LNCS, pages 222–236. Springer, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. M. Carbone, K. Honda, and N. Yoshida. Structured communicationcentered programming for web services. ACM Trans. Program. Lang. Syst., 34(2):8, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  8. B. Courcelle. Fundamental properties of infinite trees. Theoretical Comput. Sci., 25:95–169, 1983.Google ScholarGoogle ScholarCross RefCross Ref
  9. S. J. Gay. Bounded polymorphism in session types. Mathematical Structures in Computer Science, 18(5):895–930, 2008.Google ScholarGoogle ScholarCross RefCross Ref
  10. S. J. Gay and M. Hole. Subtyping for session types in the pi calculus. Acta Informaticæ, 42(2-3):191–225, 2005.Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. S. J. Gay and V. T. Vasconcelos. Linear type theory for asynchronous session types. J. Funct. Program., 20(1):19–50, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  13. K. Honda. Types for dyadic interaction. In CONCUR, volume 715 of LNCS, pages 509–523. Springer, 1993. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  15. K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In POPL, pages 273–284. ACM, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  17. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  18. B. C. Pierce. Types and Programming Languages. MIT Press, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. J. H. Reppy. CML: A higher-order concurrent language. In PLDI, pages 293–305. ACM, 1991. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. D. Sangiorgi. An Introduction to Bisimulation and Coinduction. Cambridge University Press, 2014. ISBN 9781139161381. Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  22. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  23. P. Wadler. Propositions as sessions. J. Funct. Program., 24(2-3):384– 418, 2014.Google ScholarGoogle ScholarCross RefCross Ref
  24. D. Walker. Advanced Topics in Types and Programming Languages, chapter Substructural Type Systems. MIT Press, 2005.Google ScholarGoogle Scholar

Index Terms

  1. Context-free session types

        Recommendations

        Comments

        Login options

        Check if you have access through your login credentials or your institution to get full access on this article.

        Sign in
        • Published in

          cover image ACM Conferences
          ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
          September 2016
          501 pages
          ISBN:9781450342193
          DOI:10.1145/2951913

          Copyright © 2016 ACM

          Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

          Publisher

          Association for Computing Machinery

          New York, NY, United States

          Publication History

          • Published: 4 September 2016

          Permissions

          Request permissions about this article.

          Request Permissions

          Check for updates

          Qualifiers

          • research-article

          Acceptance Rates

          Overall Acceptance Rate333of1,064submissions,31%

          Upcoming Conference

          ICFP '24

        PDF Format

        View or Download as a PDF file.

        PDF

        eReader

        View online with eReader.

        eReader