Normalization by gluing for free {\lambda}-theories
Logic in Computer Science
2018-09-25 v1
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.
Keywords
Cite
@article{arxiv.1809.08646,
title = {Normalization by gluing for free {\lambda}-theories},
author = {Jonathan Sterling and Bas Spitters},
journal= {arXiv preprint arXiv:1809.08646},
year = {2018}
}