一句话：在类型论内部用商归纳类型构造依赖类型的正规化求值，并证明定义相等可判定。
本文为依赖类型发展基于预层范畴的正规化求值（NBE）。构造完全在类型论元语言中表述，使用商归纳类型，并采用类型化呈现，因此不引入前项或 realizer，所有构造都尊重转换关系。对于简单类型，NBE 通常依赖语法与预层解释之间的逻辑关系；作者将预层解释与逻辑关系合并为一个证明相关的逻辑谓词。基于此证明正规化、完备性、稳定性以及定义相等性的可判定性。大部分构造已在 Agda 中形式化。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{AltenkirchK16,
title = {Normalisation by Evaluation for Type Theory, in Type Theory},
author = {Thorsten Altenkirch and Ambrus Kaposi},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
year = {2017},
doi = {10.23638/lmcs-13(4:1)2017}
}