Interaction graphs: multiplicatives

DOI10.1016/J.APAL.2012.04.005MaRDI QIDQ714715zbMATHOpenAlexFDO

Authors Thomas Seiller

Publication date 11 October 2012

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

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

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)

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.

Recommendations

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

Cites work

• scientific article; zbMATH DE number 4103051 (Why is no real title available?)
• scientific article; zbMATH DE number 48576 (Why is no real title available?)
• scientific article; zbMATH DE number 194205 (Why is no real title available?)
• scientific article; zbMATH DE number 4123722 (Why is no real title available?)
• scientific article; zbMATH DE number 1074568 (Why is no real title available?)
• scientific article; zbMATH DE number 1105820 (Why is no real title available?)
• scientific article; zbMATH DE number 1479606 (Why is no real title available?)
• scientific article; zbMATH DE number 2134919 (Why is no real title available?)
• scientific article; zbMATH DE number 786499 (Why is no real title available?)
• scientific article; zbMATH DE number 5038458 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• An Explicit Framework for Interaction Nets
• Coherence in closed categories
• Determinant theory in finite factors
• Geometry of Interaction and linear combinatory algebras
• Geometry of interaction. V: Logic in the hyperfinite factor
• Linear logic
• Locus solum: From the rules of logic to the logic of rules.
• On full abstraction for PCF: I, II and III
• The blind spot. Lectures on logic
• Theory of operator algebras I.
• Theory of operator algebras. II
• Theory of operator algebras. III

Cited in

(14)

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

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)