Context-Free Session Types for Applied Pi-Calculus

Jens Aagaard
(Department of Computer Science, Aalborg University)
Hans Hüttel
(Department of Computer Science, Aalborg University)
Mathias Jakobsen
(Department of Computer Science, Aalborg University)
Mikkel Kettunen
(Department of Computer Science, Aalborg University)

We present a binary session type system using context-free session types to a version of the applied pi-calculus of Abadi et. al. where only base terms, constants and channels can be sent. Session types resemble process terms from BPA and we use a version of bisimulation equivalence to characterize type equivalence. We present a quotiented type system defined on type equivalence classes for which type equivalence is built into the type system. Both type systems satisfy general soundness properties; this is established by an appeal to a generic session type system for psi-calculi.

In Jorge A. Pérez and Simone Tini: Proceedings Combined 25th International Workshop on Expressiveness in Concurrency and 15th Workshop on Structural Operational Semantics (EXPRESS/SOS 2018), Beijing, China, September 3, 2018, Electronic Proceedings in Theoretical Computer Science 276, pp. 3–18.
Published: 24th August 2018.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: