期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2019
卷号：292
页码：104-117
DOI：10.4204/EPTCS.292.6
语种：English
出版社：Open Publishing Association
摘要：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.
