CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
  Home  \  Publications  \  Article Page Login  
banner bottom
File Top
Linearity, session types and the pi calculus

We present a type system based on session types that works on a conventional pi calculus. Types are equipped with a constructor that describes the two ends of a single communication channel, this being the only type available for describing the behaviour of channels. Session types, in turn, describe the behaviour of each individual channel end, as usual. A novel notion of typing context split allows for typing processes not typable with extant type systems. We show that our system guarantees that typed processes do not engage in races for linear resources. We assess the expressiveness of type system by providing three distinct encodings---from the pi calculus with polarised variables, from the pi calculus with accept and request primitives, and from the linear pi calculus---into our system. For each language we present operational and typing correspondences, showing that our system effectively subsumes foregoing works on linear and session types. In the case of the linear pi calculus we also provide a completeness result.

Journal: Mathematical Structures in Computer Science ( United Kingdom )

Date: 2014

    Marco Giunti, Vasco T. Vasconcelos (Faculdade de Ciências da Universidade de Lisboa)
File Bottom