Coherent interaction graphs: a nondeterministic geometry of interaction for MLL
Authors: Lê Thành Dũng Nguyễn and Thomas Seiller
Paper Information
Title: | Coherent interaction graphs: a nondeterministic geometry of interaction for MLL |
Authors: | Lê Thành Dũng Nguyễn and Thomas Seiller |
Proceedings: | Linearity/TLLA Pre-proceedings |
Editors: | Maribel Fernandez, Valeria de Paiva, Thomas Ehrhard and Lorenzo Tortora De Falco |
Keywords: | interaction graphs, geometry of interaction, correctness criteria, cographs, transcendental syntax |
Abstract: | ABSTRACT. We introduce the notion of coherent graphs, and show how those can be used to define dynamic semantics for Multiplicative Linear Logic. The models thus obtained are finite with respect to several aspects (finite graphs, finite generation of types) and thus improve in this way previous constructions by Seiller. We also discuss how the added notion of coherence can also be used to introduce non-determinism. |
Pages: | 8 |
Talk: | Jul 08 14:55 (Session 40L) |
Paper: |