2018/08/27 by Jens Aagaard, Hans Hüttel, Mathias Jakobsen +1
Computer Science · #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.276.3
published as EPTCS 276, 2018, pp. 3-18 · In Proceedings EXPRESS/SOS 2018, arXiv:1808.08071
arxiv created 2018/08/27 · arxiv updated 2018/08/28
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.