Linear logic propositions as session types

Research output: Contribution to journalArticle

23 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

Fingerprint

Linear Logic
Proposition
Type Systems
Calculus
Correspondence
Cut-elimination
Sequent Calculus
Intuitionistic Logic
Classical Logic
Deadlock
Linearity
Fidelity
Output
Alternatives
Presentation

Keywords

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

Cite this

@article{6de052a644bf4b01bb2954f5557c2d26,
title = "Linear logic propositions as session types",
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.",
keywords = "NAME-PASSING CALCULI, PI-CALCULUS, INTERNAL MOBILITY",
author = "Lu{\'i}s Caires and Frank Pfenning and Bernardo Toninho",
note = "sem pdf. Fundacao para a Ciencia e a Tecnologia through the Carnegie Mellon Portugal Program (SFRH/BD/33763/2009 INTERFACES NGN-44/2009 ; PEst-OE/EEI/UI0527/2011) Army Research Office (W911NF-09-1-0273)",
year = "2016",
month = "3",
day = "1",
doi = "10.1017/S0960129514000218",
language = "English",
volume = "26",
pages = "367--423",
journal = "Mathematical Structures in Computer Science",
issn = "0960-1295",
publisher = "Cambridge University Press",
number = "3",

}

Linear logic propositions as session types. / Caires, Luís; Pfenning, Frank; Toninho, Bernardo.

In: Mathematical Structures in Computer Science, Vol. 26, No. 3, 01.03.2016, p. 367-423.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Linear logic propositions as session types

AU - Caires, Luís

AU - Pfenning, Frank

AU - Toninho, Bernardo

N1 - sem pdf. Fundacao para a Ciencia e a Tecnologia through the Carnegie Mellon Portugal Program (SFRH/BD/33763/2009 INTERFACES NGN-44/2009 ; PEst-OE/EEI/UI0527/2011) Army Research Office (W911NF-09-1-0273)

PY - 2016/3/1

Y1 - 2016/3/1

N2 - 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.

AB - 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.

KW - NAME-PASSING CALCULI

KW - PI-CALCULUS

KW - INTERNAL MOBILITY

UR - http://www.scopus.com/inward/record.url?scp=84957625632&partnerID=8YFLogxK

U2 - 10.1017/S0960129514000218

DO - 10.1017/S0960129514000218

M3 - Article

VL - 26

SP - 367

EP - 423

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - 3

ER -