Normalization Without Syntax - Archive ouverte HAL Access content directly
Conference Papers Year :

Normalization Without Syntax


We present normalization for intuitionistic combinatorial proofs (ICPs) and relate it to the simplytyped lambda-calculus. We prove confluence and strong normalization. Combinatorial proofs, or "proofs without syntax", form a graphical semantics of proof in various logics that is canonical yet complexity-aware: they are a polynomial-sized representation of sequent proofs that factors out exactly the non-duplicating permutations. Our approach to normalization aligns with these characteristics: it is canonical (free of permutations) and generic (readily applied to other logics). Our reduction mechanism is a canonical representation of reduction in sequent calculus with closed cuts (no abstraction is allowed below a cut), and relates to closed reduction in lambda-calculus and supercombinators. While we will use ICPs concretely, the notion of reduction is completely abstract, and can be specialized to give a reduction mechanism for any representation of typed normal forms.
Fichier principal
Vignette du fichier
FSCD2022_paper_1156.pdf (685.32 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03654060 , version 1 (28-04-2022)


  • HAL Id : hal-03654060 , version 1


Willem Heijltjes, Dominic Hughes, Lutz Strassburger. Normalization Without Syntax. FSCD 2022, Aug 2022, Haifa, Israel. ⟨hal-03654060⟩
53 View
84 Download


Gmail Facebook Twitter LinkedIn More