Context-Free Session Types

作者：Thiemann Peter^*; Vasconcelos Vasco T

来源：ACM Sigplan Notices, 2016, 51(9): 462-475.

DOI：10.1145/2951913.2951926

• session types
• semantics
• type checking

Session types describe structured communication on heteroge-neously 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.

• 出版日期2016-9