Normalisation by Evaluation for Type Theory, in Type Theory
Logic in Computer Science
2023-06-22 v4
Abstract
We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction, and every construction respects the conversion relation. NBE for simple types uses a logical relation between the syntax and the presheaf interpretation. In our construction, we merge the presheaf interpretation and the logical relation into a proof-relevant logical predicate. We prove normalisation, completeness, stability and decidability of definitional equality. Most of the constructions were formalized in Agda.
Keywords
Cite
@article{arxiv.1612.02462,
title = {Normalisation by Evaluation for Type Theory, in Type Theory},
author = {Thorsten Altenkirch and Ambrus Kaposi},
journal= {arXiv preprint arXiv:1612.02462},
year = {2023}
}