## Description

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].Period | 17. Sept 2020 |
---|---|

Held at | Warsaw University of Technology, Poland |

Degree of Recognition | International |