Intuitionistic proofs without syntax

Willem Heijltjes, Dominic Hughes, Lutz Strassburger

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

5 Citations (SciVal)
59 Downloads (Pure)


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 languageEnglish
Title of host publication2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019
Number of pages13
ISBN (Electronic)9781728136080
ISBN (Print)9781728136097
Publication statusPublished - 6 Aug 2019
EventThirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science - Vancouver, Canada
Duration: 24 Jun 201927 Jun 2019

Publication series

NameAnnual Symposium on Logic in Computer Science
ISSN (Print)1043-6871


ConferenceThirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS


  • intuitionistic logic
  • proof nets
  • game semantics

ASJC Scopus subject areas

  • Software
  • Mathematics(all)


Dive into the research topics of 'Intuitionistic proofs without syntax'. Together they form a unique fingerprint.

Cite this