A logical reconstruction of the π-calculus and its behavioural theory

Beskrivelse

We present Hypersequent Classical Processes (HCP), a revised interpretation of the “Proofs as Processes” correspondence between linear logic and the π-calculus initially proposed by Abramsky [1994], and later developed by Bellin and Scott [1994], Caires and Pfenning [2010], and Wadler [2014], among others. HCP mends the discrepancies between linear logic and the syntax and observable semantics of parallel composition in the π-calculus, by conservatively extending linear logic to hyperenvironments (collections of environments, inspired by the hypersequents by Avron [1991]). Separation of environments in hyperenvironments is internalised by ⊗ and corresponds to parallel process behaviour. Thanks to this property, for the first time we are able to extract a labelled transition system (lts) semantics from proof rewritings. This leads to a logical reconstruction of a behavioural theory for the π-calculus corresponding to linear logic. We discuss extensions of HCP based on the logical reconstruction extension of the π-calculus like Higher Order communication by Sangiorgi [1993] and non-blocking I/O by Merro and Sangiorgi [2004].

Periode	25. feb. 2020
Sted for afholdelse	University of Glasgow, Storbritannien
Grad af anerkendelse	International