Projects per year
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.
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 | |
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
- General Mathematics
Fingerprint
Dive into the research topics of 'Intuitionistic proofs without syntax'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Typed Lambda-Calculi with Sharing and Unsharing
Heijltjes, W. (PI)
Engineering and Physical Sciences Research Council
1/01/19 → 30/07/22
Project: Research council
Profiles
-
Willem Heijltjes
- Department of Computer Science - Senior Lecturer
- Mathematical Foundations of Computation
Person: Research & Teaching