Polymorphic lambda calculus with context-free session types

Abstract: Session types provide a typing discipline for structured communication on bidirectional channels. Context-free session types overcome the restriction to tail recursive protocols characteristic of conventional session types. This extension enables the serialization and deserialization of tree structures in a fully type-safe manner.

We present the theory underlying the language FreeST 2, which features context-free session types in an extension of System F with linear types and a kinding system to distinguish message types, session types, and channel types. The system presents metatheoretical challenges which we address: contractivity in the presence of polymorphism, a non-trivial equational theory on types, and decidability of type equivalence. We also establish standard results on typing preservation, progress, and a characterization of erroneous processes

Object Details

• Location: Deutsche Nationalbibliothek Frankfurt am Main
• Extent: Online-Ressource
• Language: Englisch
• Notes: ISSN: 1090-2651

Contributors, Places and Time

• Event: Veröffentlichung
• (where): Freiburg
• (who): Universität
• (when): 2024
• Creator: Almeida, Bernardo ; Mordido, Andreia ; Thiemann, Peter ; Vasconcelos, Vasco

Further information

• DOI: 10.1016/j.ic.2022.104948
• URN: urn:nbn:de:bsz:25-freidok-2455031
• Rights: Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
• Last update: 14.08.2025, 10:45 AM CEST