HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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'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.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-02386878
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Friday, November 29, 2019 - 3:00:19 PM
Last modification on : Wednesday, February 2, 2022 - 3:55:18 PM

File

icp.pdf
Files produced by the author(s)

Identifiers

Citation

Lutz Straßburger, Willem Heijltjes, Dominic Hughes. Intuitionistic proofs without syntax. LICS 2019 - 34th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2019, Vancouver, Canada. pp.1-13, ⟨10.1109/LICS.2019.8785827⟩. ⟨hal-02386878⟩

Share

Metrics

Record views

84

Files downloads

163