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

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. |

Published: 15th April 2019.

ArXived at: http://dx.doi.org/10.4204/EPTCS.292.6 | bibtex | |

Comments and questions to: eptcs@eptcs.org |

For website issues: webmaster@eptcs.org |