Intuitionistic proofs without syntax

Willem Heijltjes; Dominic Hughes; Lutz Strassburger

doi:10.1109/LICS.2019.8785827

Intuitionistic proofs without syntax

Willem Heijltjes, Dominic Hughes, Lutz Strassburger

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

3 Citations (SciVal)

44 Downloads (Pure)

Abstract

We present Intuitionistic Combinatorial Proofs (ICPs), a concrete geometric semantics of intuitionistic logic based on the principles of the second author’s classical Com- binatorial Proofs.
An ICP naturally factorizes into a linear fragment, a graphical abstraction of an IMLL proof net (an arena net), and a parallel contraction-weakening fragment (a skew fibration). ICPs relate to game semantics, and can be seen as a strategy in a Hyland-Ong arena, generalized from a tree-like to a dag-like strategy.

Our first main result, Polynomial Full Completeness, is that ICPs as a semantics are complexity-aware: the translations to and from sequent calculus are size-preserving (up to a polynomial). By contrast, lambda-calculus and game semantics incur an exponential blowup. Our second main result, Local Canonicity, is that ICPs abstract fully and faithfully over the non-duplicating permutations of the sequent calculus, analogously to the first and second authors’ recent result for MALL.

Original language	English
Title of host publication	2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019
Publisher	IEEE
Pages	1-13
Number of pages	13
ISBN (Electronic)	9781728136080
ISBN (Print)	9781728136097
DOIs	https://doi.org/10.1109/LICS.2019.8785827
Publication status	Published - 6 Aug 2019
Event	Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science - Vancouver, Canada Duration: 24 Jun 2019 → 27 Jun 2019

Publication series

Name	Annual Symposium on Logic in Computer Science
Volume	2019-June
ISSN (Print)	1043-6871

Conference

Conference	Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated title	LICS
Country/Territory	Canada
City	Vancouver
Period	24/06/19 → 27/06/19

Keywords

intuitionistic logic
proof nets
game semantics

ASJC Scopus subject areas

Software
Mathematics(all)

Access to Document

10.1109/LICS.2019.8785827

icp.PDF
(C) IEEE 2019. Personal use of this material is permitted. Permission from IEEE must be obtained for all other users, including reprinting/ republishing this material for advertising or promotional purposes, creating new collective works for resale or redistribution to servers or lists, or reuse of any copyrighted components of this work in other works.
Accepted author manuscript, 377 KB

Cite this

Intuitionistic proofs without syntax. / Heijltjes, Willem; Hughes, Dominic; Strassburger, Lutz.

2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. IEEE, 2019. p. 1-13 (Annual Symposium on Logic in Computer Science; Vol. 2019-June).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Heijltjes, W, Hughes, D & Strassburger, L 2019, Intuitionistic proofs without syntax. in 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. Annual Symposium on Logic in Computer Science, vol. 2019-June, IEEE, pp. 1-13, Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science, Vancouver, Canada, 24/06/19. https://doi.org/10.1109/LICS.2019.8785827

@inproceedings{c8ba36667e5047db8a1be81ceaf71162,

title = "Intuitionistic proofs without syntax",

abstract = "We present Intuitionistic Combinatorial Proofs (ICPs), a concrete geometric semantics of intuitionistic logic based on the principles of the second author{\textquoteright}s classical Com- binatorial Proofs.An ICP naturally factorizes into a linear fragment, a graphical abstraction of an IMLL proof net (an arena net), and a parallel contraction-weakening fragment (a skew fibration). ICPs relate to game semantics, and can be seen as a strategy in a Hyland-Ong arena, generalized from a tree-like to a dag-like strategy.Our first main result, Polynomial Full Completeness, is that ICPs as a semantics are complexity-aware: the translations to and from sequent calculus are size-preserving (up to a polynomial). By contrast, lambda-calculus and game semantics incur an exponential blowup. Our second main result, Local Canonicity, is that ICPs abstract fully and faithfully over the non-duplicating permutations of the sequent calculus, analogously to the first and second authors{\textquoteright} recent result for MALL.",

keywords = "intuitionistic logic, proof nets, game semantics",

author = "Willem Heijltjes and Dominic Hughes and Lutz Strassburger",

year = "2019",

month = aug,

day = "6",

doi = "10.1109/LICS.2019.8785827",

language = "English",

isbn = "9781728136097",

series = "Annual Symposium on Logic in Computer Science",

publisher = "IEEE",

pages = "1--13",

booktitle = "2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019",

address = "USA United States",

note = "Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ; Conference date: 24-06-2019 Through 27-06-2019",

}

TY - GEN

T1 - Intuitionistic proofs without syntax

AU - Heijltjes, Willem

AU - Hughes, Dominic

AU - Strassburger, Lutz

PY - 2019/8/6

Y1 - 2019/8/6

N2 - We present Intuitionistic Combinatorial Proofs (ICPs), a concrete geometric semantics of intuitionistic logic based on the principles of the second author’s classical Com- binatorial Proofs.An ICP naturally factorizes into a linear fragment, a graphical abstraction of an IMLL proof net (an arena net), and a parallel contraction-weakening fragment (a skew fibration). ICPs relate to game semantics, and can be seen as a strategy in a Hyland-Ong arena, generalized from a tree-like to a dag-like strategy.Our first main result, Polynomial Full Completeness, is that ICPs as a semantics are complexity-aware: the translations to and from sequent calculus are size-preserving (up to a polynomial). By contrast, lambda-calculus and game semantics incur an exponential blowup. Our second main result, Local Canonicity, is that ICPs abstract fully and faithfully over the non-duplicating permutations of the sequent calculus, analogously to the first and second authors’ recent result for MALL.

AB - We present Intuitionistic Combinatorial Proofs (ICPs), a concrete geometric semantics of intuitionistic logic based on the principles of the second author’s classical Com- binatorial Proofs.An ICP naturally factorizes into a linear fragment, a graphical abstraction of an IMLL proof net (an arena net), and a parallel contraction-weakening fragment (a skew fibration). ICPs relate to game semantics, and can be seen as a strategy in a Hyland-Ong arena, generalized from a tree-like to a dag-like strategy.Our first main result, Polynomial Full Completeness, is that ICPs as a semantics are complexity-aware: the translations to and from sequent calculus are size-preserving (up to a polynomial). By contrast, lambda-calculus and game semantics incur an exponential blowup. Our second main result, Local Canonicity, is that ICPs abstract fully and faithfully over the non-duplicating permutations of the sequent calculus, analogously to the first and second authors’ recent result for MALL.

KW - intuitionistic logic

KW - proof nets

KW - game semantics

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

U2 - 10.1109/LICS.2019.8785827

DO - 10.1109/LICS.2019.8785827

M3 - Chapter in a published conference proceeding

SN - 9781728136097

T3 - Annual Symposium on Logic in Computer Science

SP - 1

EP - 13

BT - 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019

PB - IEEE

T2 - Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science

Y2 - 24 June 2019 through 27 June 2019

ER -

Intuitionistic proofs without syntax

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Typed Lambda-Calculi with Sharing and Unsharing

Willem Heijltjes

Cite this

Intuitionistic proofs without syntax

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

Typed Lambda-Calculi with Sharing and Unsharing

Profiles

Willem Heijltjes

Cite this