2026-07-25T03:07:49Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16300 2024-03-06T10:57:10Z ddc:004 open_access

Normalization Without Syntax Heijltjes, Willem B. Hughes, Dominic J. D. Straßburger, Lutz combinatorial proofs intuitionistic logic lambda-calculus Curry-Howard proof nets We present normalization for intuitionistic combinatorial proofs (ICPs) and relate it to the simply-typed 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Willem B. Heijltjes and Dominic J. D. Hughes and Lutz Straßburger 2022 Is Part Of LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2022.19 urn:nbn:de:0030-drops-163004 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.19 eng https://creativecommons.org/licenses/by/4.0/legalcode