Normalization Without Syntax

Willem Heijltjes, Dominic Hughes, Lutz Strassburger

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

30 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publication7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022
Subtitle of host publicationFSCD 2022
EditorsAmy P. Felty
Place of PublicationDagstuhl, Germany
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages19:1-19:19
Number of pages19
Volume228
Edition2022
ISBN (Electronic)978-3-95977-233-4
DOIs
Publication statusPublished - 28 Jun 2022

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume228
ISSN (Print)1868-8969

Bibliographical note

Funding Information:
Funding Supported by EPSRC Grant EP/R029121/1 Typed Lambda-Calculi with Sharing and Unsharing and Inria Associated Team Combinatorial Proof Normalization (COMPRONOM).

Publisher Copyright:
© Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger

Keywords

  • Curry–Howard
  • combinatorial proofs
  • intuitionistic logic
  • lambda-calculus
  • proof nets

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Normalization Without Syntax'. Together they form a unique fingerprint.

Cite this