Pith. sign in

REVIEW 1 cited by

Normalization by gluing for free {λ}-theories

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1809.08646 v1 pith:XACVXGNE submitted 2018-09-23 cs.LO

Normalization by gluing for free {λ}-theories

Jonathan Sterling , Bas Spitters This is my paper
classification cs.LO
keywords normalizationgluingevaluationsemanticcloselyconnectionconstructionscorresponds
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved
0 comments
read the original 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.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Directed proof-relevant logical relations in simplicial HoTT

    cs.LO 2026-07 accept novelty 7.5 partial

    Contravariant families in simplicial HoTT supply proof-relevant expansion, yielding directed Boolean canonicity and a binary parametricity model over reduction-aware syntax.