Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Fri 18 Jan 2019 13:45 - 14:07 at Sala I - Semantics Chair(s): Noam Zeilberger

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. Leveraging the information on parallelism at the level of types, we obtain a logical reconstruction of the delayed actions that Merro and Sangiorgi [2004] formulated to model non-blocking I/O in the π-calculus. We define a denotational semantics for processes based on Brzozowski derivatives, and uncover that non-interference in HCP corresponds to Fubini’s theorem of double antiderivation. Having an lts allows us to validate HCP using the standard toolbox of behavioural theory. We instantiate bisimilarity and barbed congruence for HCP, and obtain a full abstraction result: bisimilarity, denotational equivalence, and barbed congruence coincide.

Fri 18 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

13:45 - 14:51: SemanticsResearch Papers at Sala I
Chair(s): Noam ZeilbergerUniversity of Birmingham, UK
13:45 - 14:07
Better Late Than Never: A Fully Abstract Semantics for Classical Processes
Research Papers
Wen KokkeUniversity of Edinburgh, Fabrizio MontesiUniversity of Southern Denmark, Marco PeressottiUniversity of Southern Denmark
Link to publication DOI Media Attached
14:07 - 14:29
Diagrammatic Algebra: From Linear to Concurrent Systems
Research Papers
Filippo BonchiUniversity of Pisa, Joshua HollandUniversity of Southampton, Robin PiedeleuUniversity of Oxford, Pawel SobocinskiUniversity of Southampton, Fabio ZanasiUniversity College London
Link to publication DOI Media Attached
14:29 - 14:51
Fixpoint Games on Continuous Lattices
Research Papers
Paolo BaldanUniversity of Padova, Barbara KönigUniversity of Duisburg-Essen, Christina Mika-MichalskiUniversity of Duisburg-Essen, Tommaso PadoanUniversity of Padova
Link to publication DOI Media Attached File Attached