Skip to Main content Skip to Navigation
Conference papers

A type checking algorithm for qualified session types

Marco Giunti 1, *
* Corresponding author
1 COMETE - Concurrency, Mobility and Transactions
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
Abstract : We present a type checking algorithm for establishing a session-based discipline in the pi calculus of Milner, Parrow and Walker. Our session types are qualified as linear or unrestricted. Linearly typed communication channels are guaranteed to occur in exactly one thread, possibly multiple times; afterwards they evolve as unrestricted channels. Session protocols are described by a type constructor that denotes the two ends of one and the same communication channel. We ensure the soundness of the algorithm by showing that processes consuming all linear resources are accepted by a typing system preserving typings during the computation and that type checking is consistent with respect to structural congruence.
Document type :
Conference papers
Complete list of metadatas

Cited literature [15 references]  Display  Hide  Download
Contributor : Marco Giunti <>
Submitted on : Wednesday, November 23, 2011 - 3:01:22 PM
Last modification on : Thursday, March 5, 2020 - 6:21:30 PM
Long-term archiving on: : Friday, February 24, 2012 - 2:27:26 AM


Files produced by the author(s)




Marco Giunti. A type checking algorithm for qualified session types. 7th International Workshop on Automated Specification and Verification of Web Systems, Jun 2011, Reykjavik, Iceland. ⟨10.4204/EPTCS.61.7⟩. ⟨hal-00644061⟩



Record views


Files downloads