Algorithmic type checking for a pi-calculus with name matching and session types

摘要

We present a type checking algorithm for establishing a session-based discipline in a n -calculus with name matching. We account for analysing processes exhibiting different behaviours in the branches of the if-then-else by imposing an affine discipline for session types. This permits to obtain type-safety or absence of communication errors while accepting processes of the form if x = y then P else 0 that install a session protocol P whenever the test succeeds, and abort otherwise. To this aim we define a type system based on a notion of context split, and we prove that it satisfies subject reduction and type-safety. We implement the type system in a split-free type checking algorithm, and we prove that processes accepted by the algorithm are well-typed. We then show that processes that are typed and do not contain Wait for deadlocks - an input and its corresponding output (or vice versa) are in the same thread instead of in parallel ones - are accepted by the algorithm, thus providing a partial completeness result. We conclude by investigating the expressiveness of the typing system and show that our theory subsumes recent works on linear and session types.