Coherent Interaction Graphs

Lê Thành Dũng Nguyen
(LIPN, Université Paris 13)
Thomas Seiller

We introduce the notion of coherent graphs, and show how those can be used to define dynamic semantics for Multiplicative Linear Logic (MLL) extended with non-determinism. Thanks to the use of a coherence relation rather than mere formal sums of non-deterministic possibilities, our model enjoys some finiteness and sparsity properties.

We also show how studying the semantic types generated by a single "test" within our model of MLL naturally gives rise to a notion of proof net, which turns out to be exactly Retoré's R&B-cographs. This revisits the old idea that multplicative proof net correctness is interactive, with a twist: types are characterized not by a set of counter-proofs but by a single non-deterministic counter-proof.

In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva and Lorenzo Tortora de Falco: Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA 2018), Oxford, UK, 7-8 July 2018, Electronic Proceedings in Theoretical Computer Science 292, pp. 104–117.
Published: 15th April 2019.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: