file.pdf (233.92 kB)
Download fileSession Types as Intuitionistic Linear Propositions
journal contribution
posted on 2007-02-01, 00:00 authored by Luis Caires, Frank PfenningSeveral type disciplines for π-calculi have been proposed in which linearity plays a key
role, even if their precise relationship with pure linear logic is still not well understood.
In this paper, we introduce a type system for the π-calculus that exactly corresponds
to the standard sequent calculus proof system for dual intuitionistic linear logic. Our
type system is based on a new interpretation of linear propositions as session types, and
provides the first purely logical account of all (both shared and linear) features of session
types. We show that our type discipline is useful from a programming perspective, and
ensures session fidelity, absence of deadlocks, and a tight operational correspondence
between π-calculus reductions and cut elimination steps.