Context-Free Session Types for Applied Pi-Calculus
Logic in Computer Science
2018-08-28 v1 Programming Languages
Abstract
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.
Keywords
Cite
@article{arxiv.1808.08648,
title = {Context-Free Session Types for Applied Pi-Calculus},
author = {Jens Aagaard and Hans Hüttel and Mathias Jakobsen and Mikkel Kettunen},
journal= {arXiv preprint arXiv:1808.08648},
year = {2018}
}
Comments
In Proceedings EXPRESS/SOS 2018, arXiv:1808.08071