Linearity, session types and the Pi calculus

摘要

We present a type system based on session types that works on a conventional pi calculus.rnTypes are equipped with a constructor that describes the two ends of a singlerncommunication channel, this being the only type available for describing the behaviour ofrnchannels. Session types, in turn, describe the behaviour of each individual channel end, asrnusual. A novel notion of typing context split allows for typing processes not typable withrnextant type systems. We show that our system guarantees that typed processes do notrnengage in races for linear resources. We assess the expressiveness of the type system byrnproviding three distinct encodings – from the pi calculus with polarized variables, from thernpi calculus with accept and request primitives, and from the linear pi calculus – into ourrnsystem. For each language we present operational and typing correspondences, showing thatrnour system effectively subsumes foregoing works on linear and session types. In the case ofrnthe linear pi calculus we also provide a completeness result.