A type checking algorithm for qualified session types

Marco Giunti 1, *
* Auteur correspondant
1 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Communication dans un congrès
Laura Kovács, Rosario Pugliese, Francesco Tiezzi. 7th International Workshop on Automated Specification and Verification of Web Systems, Jun 2011, Reykjavik, Iceland. Electronic Proceedings in Theoretical Computer Science, 2011, 〈10.4204/EPTCS.61.7〉
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00644061
Contributeur : Marco Giunti <>
Soumis le : mercredi 23 novembre 2011 - 15:01:22
Dernière modification le : jeudi 10 mai 2018 - 02:06:56
Document(s) archivé(s) le : vendredi 24 février 2012 - 02:27:26

Fichiers

wwv.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Marco Giunti. A type checking algorithm for qualified session types. Laura Kovács, Rosario Pugliese, Francesco Tiezzi. 7th International Workshop on Automated Specification and Verification of Web Systems, Jun 2011, Reykjavik, Iceland. Electronic Proceedings in Theoretical Computer Science, 2011, 〈10.4204/EPTCS.61.7〉. 〈hal-00644061〉

Partager

Métriques

Consultations de la notice

383

Téléchargements de fichiers

259