A type checking algorithm for qualified session types

International audience 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, pos...

Full description

Bibliographic Details
Published in:Electronic Proceedings in Theoretical Computer Science
Main Author: Giunti, Marco
Other Authors: Concurrency, Mobility and Transactions (COMETE), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'informatique de l'École polytechnique Palaiseau (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Laura Kovács, Rosario Pugliese, Francesco Tiezzi, European Project:
Format: Conference Object
Language:English
Published: HAL CCSD 2011
Subjects:
Session types
pi calculus
type systems
program analysis
programming languages
logics of programs
computer security
ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.2: Semantics of Programming Languages/F.3.2.5: Program analysis
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Iceland
Online Access:https://hal.inria.fr/hal-00644061
https://hal.inria.fr/hal-00644061/document
https://hal.inria.fr/hal-00644061/file/wwv.pdf
https://doi.org/10.4204/EPTCS.61.7
Description
Summary:International audience 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.

Similar Items