DescriptionWe present Hypersequent Classical Processes (HCP), a revised interpretation of the “Proofs as Processes” correspondence between linear logic and the π-calculus initially proposed by Abramsky , and later developed by Bellin and Scott , Caires and Pfenning , and Wadler , 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 ). 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  and non-blocking I/O by Merro and Sangiorgi .
|Period||17. Sept 2020|
|Held at||Warsaw University of Technology, Poland|
|Degree of Recognition||International|