Published in

Elsevier Masson, Annals of Pure and Applied Logic, 12(163), p. 1808-1837

DOI: 10.1016/j.apal.2012.04.005

Links

Tools

Export citation

Search in Google Scholar

Interaction Graphs: Multiplicatives

Journal article published in 2012 by Thomas Seiller ORCID
This paper is made freely available by the publisher.
This paper is made freely available by the publisher.

Full text: Download

Green circle
Preprint: archiving allowed
Green circle
Postprint: archiving allowed
Red circle
Published version: archiving forbidden
Data provided by SHERPA/RoMEO

Abstract

We introduce a graph-theoretical representation of proofs of multiplicative linear logic which yields both a denotational semantics and a notion of truth. For this, we use a locative approach (in the sense of ludics, Girard, 2001 [11]) related to game semantics (Hyland and Ong, 2000 [17], Abramsky et al., 1994 [2]) and the Danos–Regnier interpretation of GoI operators as paths in proof nets (Asperti et al., 1994 [3], Danos and Regnier, 1995 [4]). We show how we can retrieve from this locative framework both a categorical semantics for Multiplicative Linear Logic (MLL) with distinct units and a notion of truth. Moreover, we show how a restricted version of our model can be reformulated in the exact same terms as Girardʼs geometry of interaction (Girard, 2011 [14]). This shows that this restriction of our framework gives a combinatorial approach to J.-Y. Girardʼs geometry of interaction in the hyperfinite factor, while using only graph-theoretical notions.