Normalization by gluing for free {\lambda}-theories
Jonathan Sterling, Bas Spitters
TL;DR
This paper presents an elementary gluing technique that bridges semantic normalization proofs and syntactic normalization by evaluation for free λ-theories, clarifying their connection.
Contribution
It introduces a simplified gluing method that aligns semantic and syntactic normalization approaches in λ-theories.
Findings
The gluing technique closely matches semantic normalization proofs.
The approach simplifies the connection between evaluation and normalization.
It provides an elementary framework for normalization in λ-theories.
Abstract
The connection between normalization by evaluation, logical predicates and semantic gluing constructions is a matter of folklore, worked out in varying degrees within the literature. In this note, we present an elementary version of the gluing technique which corresponds closely with both semantic normalization proofs and the syntactic normalization by evaluation.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Homotopy and Cohomology in Algebraic Topology