Interaction graphs: multiplicatives

DOI10.1016/J.APAL.2012.04.005zbMATH Open1252.03143arXiv1205.6558OpenAlexW1971681260MaRDI QIDQ714715FDOQ714715

Authors: Thomas Seiller 

Publication date: 11 October 2012

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

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) related to game semantics and the Danos-Regnier interpretation of GoI operators as paths in proof nets. We show how we can retrieve from this locative framework both a categorical semantics for 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 latest geometry of interaction. 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.

Full work available at URL: https://arxiv.org/abs/1205.6558

Recommendations

• Interaction graphs: graphings
• Interaction graphs: additives
• Coherent interaction graphs
• Interaction graphs: full linear logic
• Proof diagrams for multiplicative linear logic

zbMATH Keywords

proof theoryoperator algebrascut eliminationdenotational semanticsgeometry of interactionproof netsmultiplicative linear logic

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Semantics in the theory of computing (68Q55)

Cites Work

• Theory of operator algebras. II
• On full abstraction for PCF: I, II and III
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Linear logic
• Theory of operator algebras I.
• Title not available (Why is that?)
• Geometry of Interaction and linear combinatory algebras
• Title not available (Why is that?)
• Geometry of interaction. V: Logic in the hyperfinite factor
• Locus solum: From the rules of logic to the logic of rules.
• The blind spot. Lectures on logic
• Determinant theory in finite factors
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theory of operator algebras. III
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Coherence in closed categories
• Title not available (Why is that?)
• An Explicit Framework for Interaction Nets

Cited In (14)

• Interaction graphs: full linear logic
• Title not available (Why is that?)
• Logarithmic space and permutations
• Geometry of interaction. V: Logic in the hyperfinite factor
• Computer Science Logic
• Interaction graphs: additives
• Zeta functions and the (linear) logic of Markov processes
• A correspondence between maximal abelian sub-algebras and linear logic fragments
• Title not available (Why is that?)
• Geometry of interaction for MALL via Hughes-Van Glabbeek proof-nets
• Interaction graphs: graphings
• Characterizingco-NLby a group action
• Interaction graphs: exponentials
• Commutative Locative Quantifiers for Multiplicative Linear Logic

This page was built for publication: Interaction graphs: multiplicatives

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q714715)