The paper “Polymorphic higher-order context-free session types”, authored by LASIGE’s integrated researchers Diana Costa, Andreia Mordido, Diogo Poças, and Vasco T. Vasconcelos, has been published in Theoretical Computer Science, a top-ranked journal.

The authors present an extension of polymorphic context-free session types that allows passing channels on channels, commonly known as higher-order session types. The mixture of functional types and session types has proven to be a challenge for type equivalence formulation: whereas functional type equivalence is often inductive and presented as a system of derivation rules, session type equivalence is often coinductive and usually presented as a bisimulation. The authors propose a unifying approach that handles the equivalence of functional and higher-order context-free session types together in the form of a system of rules generating a conductively defined relation. Decidability of type equivalence is obtained via reduction to bisimulation for simple grammars, for which practical algorithms are known. To bridge the gap between types and simple grammars, the authors introduce a language of types with canonical names instead of bindings (which they call c-types), and propose a notion of canonical renaming to translate types to c-types.

The paper is available here.