Linear logic propositions as session types

Research output: Contribution to journalArticle

26 Citations (Scopus)

Abstract

Throughout the years, several typing disciplines for the π-calculus have been proposed. Arguably, the most widespread of these typing disciplines consists of session types. Session types describe the input/output behaviour of processes and traditionally provide strong guarantees about this behaviour (i.e. deadlock-freedom and fidelity). While these systems exploit a fundamental notion of linearity, the precise connection between linear logic and session types has not been well understood. This paper proposes a type system for the π-calculus that corresponds to a standard sequent calculus presentation of intuitionistic linear logic, interpreting linear propositions as session types and thus providing a purely logical account of all key features and properties of session types. We show the deep correspondence between linear logic and session types by exhibiting a tight operational correspondence between cut-elimination steps and process reductions. We also discuss an alternative presentation of linear session types based on classical linear logic, and compare our development with other more traditional session type systems.

Original languageEnglish
Pages (from-to)367-423
Number of pages57
JournalMathematical Structures in Computer Science
Volume26
Issue number3
DOIs
Publication statusPublished - 1 Mar 2016

Keywords

  • NAME-PASSING CALCULI
  • PI-CALCULUS
  • INTERNAL MOBILITY

Fingerprint Dive into the research topics of 'Linear logic propositions as session types'. Together they form a unique fingerprint.

  • Cite this