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
Contributor : Lutz Straßburger <>
Submitted on : Friday, November 29, 2019 - 3:00:19 PM
Last modification on : Thursday, January 7, 2021 - 3:40:15 PM


Files produced by the author(s)




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⟩



Record views


Files downloads