Enguerrand Prebet (ENS de Lyon), Sequentiality, References and Well-bracketing in the pi-calculus

Schedule

Abstract

The pi-calculus is used as a model for programming languages. Its contexts exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable behavioural equivalences in cases when more disciplined contexts are expected. We formalise using types three different disciplines: sequentiality or the idea of having a single thread of computation ; reference types for which channels behave like bits of store or atomic register ; and well-bracketing which strengthens the sequentiality constraints to also obey a stack-like discipline. For each, we present the type system along with its consequences on behavioural equivalence and the corresponding bisimulation techniques.