Interaction graphs: full linear logic

DOI10.1145/2933575.2934568zbMATH Open1394.03075arXiv1504.04152OpenAlexW2964061972WikidataQ130863282 ScholiaQ130863282MaRDI QIDQ4635900FDOQ4635900

Authors: Thomas Seiller 

Publication date: 23 April 2018

Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: Interaction graphs were introduced as a general, uniform, construction of dynamic models of linear logic, encompassing all "Geometry of Interaction" (GoI) constructions introduced so far. This series of work was inspired from Girard's hyperfinite GoI, and develops a quantitative approach that should be understood as a dynamic version of weighted relational models. Until now, the interaction graphs framework has been shown to deal with exponentials for the constrained system ELL (Elementary Linear Logic) while keeping its quantitative aspect. Adapting older constructions by Girard, one can clearly define "full" exponentials, but at the cost of these quantitative features. We show here that allowing interpretations of proofs to use continuous (yet finite in a measure-theoretic sense) sets of states, as opposed to earlier Interaction Graphs constructions were these sets of states were discrete (and finite), provides a model for full linear logic with second order quantification.

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

Recommendations

• Interaction graphs: graphings
• Interaction graphs: exponentials
• Interaction graphs: multiplicatives
• A categorical model for the geometry of interaction
• Interaction graphs: additives

zbMATH Keywords

linear logicmeasurable dynamicsgeometry of interactioninteraction graphsquantitative semantics

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Cited In (6)

• Interaction nets for linear logic
• Interaction graphs: multiplicatives
• Distributing and parallelizing non-canonical loops
• Global view on reactivity: switch graphs and their logics
• Title not available (Why is that?)
• Unifying lower bounds for algebraic machines, semantically

This page was built for publication: Interaction graphs: full linear logic

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