Context-Free Session Types for Applied Pi-Calculus

TL;DR

This paper introduces a novel binary session type system using context-free session types within the applied pi-calculus, enabling precise type equivalence and soundness proofs for process communication modeling.

Contribution

It proposes a new session type system based on context-free types for applied pi-calculus, incorporating type equivalence into the type system itself.

Findings

Type systems satisfy soundness properties

Type equivalence characterized by bisimulation

Type system built on type equivalence classes

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.