Session Types as Intuitionistic Linear Propositions

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Several 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.
Original languageUnknown
Title of host publicationLecture Notes in Computer Science
Pages222-236
DOIs
Publication statusPublished - 1 Jan 2010
EventInternational Conference on Concurrency Theory (Concur 2010) -
Duration: 1 Jan 2010 → …

Conference

ConferenceInternational Conference on Concurrency Theory (Concur 2010)
Period1/01/10 → …

Cite this