π-calculus, Session Types research at Imperial College

Full completeness and injectivity (unit-free multiplicative-additive fragment)

Commuting conversions of Linear Logic induce a notion of dependency between rules inside a proof derivation: a rule depends on a previous rule when they cannot be permuted using the conversions. We propose a new interpretation of proofs of Linear Logic as causal invariants which captures exactly this dependency.

We represent causal invariants using game semantics based on general event structures, carving out, inside a recent game semantics model based on general event structures, a submodel of causal invariants. This submodel supports an interpretation of unit-free Multiplicative Additive Linear Logic with MIX (MALL⁻) which is (1) fully complete: every element of the model is the denotation of a proof and (2) injective: equality in the model characterises exactly commuting conversions of MALL⁻. This improves over the standard fully complete game semantics model of MALL⁻.

@inproceedings{CY2019, author = {Simon Castellan and Nobuko Yoshida}, title = {{Causality in Linear Logic}}, booktitle = {22nd International Conference on Foundations of Software Science and Computation Structures}, series = {LNCS}, pages = {150--168}, publisher = {Springer}, year = 2019 }

@inproceedings{CY2019, author = {Simon Castellan and Nobuko Yoshida}, title = {{Causality in Linear Logic}}, booktitle = {22nd International Conference on Foundations of Software Science and Computation Structures}, series = {LNCS}, pages = {150--168}, publisher = {Springer}, doi = "10.1007/978-3-030-17127-8_9", year = 2019 }