Interaction graphs: full linear logic

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Standard

Interaction graphs : full linear logic. / Seiller, Thomas.

Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science. Vol. 05-08-July-2016 Association for Computing Machinery, 2016. p. 427-436.

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Harvard

Seiller, T 2016, Interaction graphs: full linear logic. in Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science. vol. 05-08-July-2016, Association for Computing Machinery, pp. 427-436, 31st Annual ACM/IEEE Symposium on Logic in Computer Science, New York, United States, 05/07/2016. https://doi.org/10.1145/2933575.2934568

APA

Seiller, T. (2016). Interaction graphs: full linear logic. In Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (Vol. 05-08-July-2016, pp. 427-436). Association for Computing Machinery. https://doi.org/10.1145/2933575.2934568

Vancouver

Seiller T. Interaction graphs: full linear logic. In Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science. Vol. 05-08-July-2016. Association for Computing Machinery. 2016. p. 427-436 https://doi.org/10.1145/2933575.2934568

Author

Seiller, Thomas. / Interaction graphs : full linear logic. Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science. Vol. 05-08-July-2016 Association for Computing Machinery, 2016. pp. 427-436

Bibtex

@inproceedings{685d0def0748497cbe2e13d01bf69263,
title = "Interaction graphs: full linear logic",
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.",
keywords = "Geometry of Interaction, Interaction Graphs, Linear Logic, Measurable Dynamics, Quantitative Semantics",
author = "Thomas Seiller",
year = "2016",
doi = "10.1145/2933575.2934568",
language = "English",
volume = "05-08-July-2016",
pages = "427--436",
booktitle = "Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science",
publisher = "Association for Computing Machinery",
note = "null ; Conference date: 05-07-2016 Through 08-07-2016",

}

RIS

TY - GEN

T1 - Interaction graphs

AU - Seiller, Thomas

N1 - Conference code: 31

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

KW - Geometry of Interaction

KW - Interaction Graphs

KW - Linear Logic

KW - Measurable Dynamics

KW - Quantitative Semantics

UR - http://www.scopus.com/inward/record.url?scp=84994607164&partnerID=8YFLogxK

U2 - 10.1145/2933575.2934568

DO - 10.1145/2933575.2934568

M3 - Article in proceedings

AN - SCOPUS:84994607164

VL - 05-08-July-2016

SP - 427

EP - 436

BT - Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science

PB - Association for Computing Machinery

Y2 - 5 July 2016 through 8 July 2016

ER -

ID: 172101845