Interaction graphs: full linear logic

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

  • Thomas Seiller

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.

Original languageEnglish
Title of host publicationProceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science
Number of pages10
Volume05-08-July-2016
PublisherAssociation for Computing Machinery
Publication date2016
Pages427-436
ISBN (Electronic)978-1-4503-4391-6
DOIs
Publication statusPublished - 2016
Event31st Annual ACM/IEEE Symposium on Logic in Computer Science - New York, United States
Duration: 5 Jul 20168 Jul 2016
Conference number: 31

Conference

Conference31st Annual ACM/IEEE Symposium on Logic in Computer Science
Nummer31
LandUnited States
ByNew York
Periode05/07/201608/07/2016

    Research areas

  • Geometry of Interaction, Interaction Graphs, Linear Logic, Measurable Dynamics, Quantitative Semantics

ID: 172101845