Detail

Binary Session Types for Psi-calculi

Binary session types can be used to describe communication protocols, and to ensure a variety of properties, e.g. deadlock freedom, liveness, or secure information flow. Session type systems are often formulated for variants of the pi-calculus, and for each such system, the central properties such as session fidelity must be re-established.

The framework of psi-calculi introduced by Bengtson et al. makes it possible to give a general account of variants of the pi-calculus. We use this framework to describe a generic session type system for variants of the ?-calculus. In this generic system, standard properties, including fidelity, hold at the level of the framework and are then guaranteed to hold when the generic system is instantiated.

We show that our system can capture existing systems including the session type system due to Gay and Hole, a type system for progress due to Vieira and Vasconcelos and a refinement type system due to Baltazar et al. The standard fidelity property is proved at the level of the generic system, and automatically hold when the system is instantiated.