一句话：提出整合高阶大小多态与依赖类型的大小类型理论，并用 NBE 判定判等、子类型和类型检查。
在依赖类型证明助手中，归纳证明即递归函数，终止检查器属于可信核心，因此大小类型被用于把终止性检查整合进类型检查。但将完整的大小类型严格整合进依赖类型理论仍属空白，难点在于证明项中显式大小会干扰判等，使语义相同的项被区分。本文整合依赖类型与带高阶大小多态的大小类型，引入两个大小量词：∀ 可在判等时忽略大小，Π 用于抽象语义相关的大小。作者为新类型理论改造 normalization-by-evaluation，采用由类型形状导向的 reflection 与 reification，从而判定判断性相等；由此可推出子类型以及正规形式的类型检查可判定，后者通过双向算法实现。
Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by induction are just recursive functional programs, the termination checker is an integral component of the trusted core, as validity of proofs depend on termination. However, a rigorous integration of full-fledged sized types into dependent type theory is lacking so far. Such an integration is non-trivial, as explicit sizes in proof terms might get in the way of equality checking, making terms appear distinct that should have the same semantics. In this article, we integrate dependent types and sized types with higher-rank size polymorphism, which is essential for generic programming and abstraction. We introduce a size quantifier ∀ which lets us ignore sizes in terms for equality checking, alongside with a second quantifier Π for abstracting over sizes that do affect the semantics of types and terms. Judgmental equality is decided by an adaptation of normalization-by-evaluation for our new type theory, which features type shape -directed reflection and reification. It follows that subtyping and type checking of normal forms are decidable as well, the latter by a bidirectional algorithm.
@article{0001VW17,
title = {Normalization by evaluation for sized dependent types},
author = {Andreas Abel and Andrea Vezzosi and Theo Winterhalter},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110277}
}