Honda, “Types for Dyadic Interaction”, CONCUR 1993.
Takeuchi, Honda & Kubo, “An Interaction-Based Language and its Typing System“, PARLE 1994.
Honda, Vasconcelos & Kubo, “Language Primitives and Type Discipline for Structured Communication-Based Programming”, ESOP 1998.
Proofs as processes
Caires & Pfenning (2010) established a correspondence between intuitionistic linear logic and session typed π-calculus. Later on, Wadler (2012) established a correspondence between classical linear logic and the same calculus.
propositions as session types
proofs as π-processes
cut reduction as communication
References
Ornela Dardha, Introduction to Session Types, (2016) (pdf).
Created on May 30, 2024 at 11:09:09.
See the history of this page for a list of all contributions to it.