Session Types as Intuitionistic Linear Propositions
By Luís Caires, Frank Pfenning. International Conference on Concurrency Theory, 2010
397 citations recorded by the source corpus.
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.
Subfields: Artificial Intelligence, Computational Theory and Mathematics
View Paper: https://www.semanticscholar.org/paper/0dac5be83a9f997ce05c1c58f588d0c45ad42a4a
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
In Computational Theory and Mathematics
- Alberto Lluch-Lafuente
- Manuel Mazzara
- Ruslan Mustafin
- Larisa Safina
- Fabrizio Montesi
- Saverio Giallorenzo
- Nicola Dragoni
Citations in the corpus
- Microservices: Yesterday, Today, and Tomorrow (2016, methodology): “A prominent example is a Curry-Howard correspondence between session types and the process model of π -calculus, given in [8] (linear logical propositions correspond to session types, and communications to proof normalization in linear logic).”
- Propositions as sessions (2012, neutral): “In Caires and Pfenning (2010), the following four rules interpret the linear connectives ⊗ and (cid:40) .”