一句话：首次为依赖类型提出带 join-point 优化的 ANF 翻译，并证明其类型保持及分离编译正确性。
许多程序员使用 Coq 等依赖类型语言做机器验证，但现有编译器在编译后及链接外部代码时不提供保证。类型保持编译器可保留类型中的保证，然而标准编译遍无法保持强度依赖类型理论（intensional dependent type theory）的依赖类型，因为该类型系统对语法变化高度敏感。本文为带布尔与自然数依赖消去的 Extended Calculus of Constructions（ECC）子集设计了一种带 join-point 优化的 A-normal form（ANF）翻译。目标语言具有 equality reflection，使类型系统能编码项的语义相等，这是证明类型保持与分离编译正确性的关键。该工作是首个面向依赖类型的 ANF 翻译，支持 universe hierarchy，且不依赖 parametricity 或 impredicativity。
Abstract Many programmers use dependently typed languages such as Coq to machine-verify high-assurance software. However, existing compilers for these languages provide no guarantees after compiling, nor when linking after compilation. Type-preserving compilers preserve guarantees encoded in types and then use type checking to verify compiled code and ensure safe linking with external code. Unfortunately, standard compiler passes do not preserve the dependent typing of commonly used (intensional) type theories. This is because assumptions valid in simpler type systems no longer hold, and intensional dependent type systems are highly sensitive to syntactic changes, including compilation. We develop an A-normal form (ANF) translation with join-point optimization—a standard translation for making control flow explicit in functional languages—from the Extended Calculus of Constructions (ECC) with dependent elimination of booleans and natural numbers (a representative subset of Coq). Our dependently typed target language has equality reflection, allowing the type system to encode semantic equality of terms. This is key to proving type preservation and correctness of separate compilation for this translation. This is the first ANF translation for dependent types. Unlike related translations, it supports the universe hierarchy, and does not rely on parametricity or impredicativity.
@article{paperbot1634,
title = {ANF preserves dependent types up to extensional equality},
author = {PAULETTE KORONKEVICH and RAMON RAKOW and AMAL AHMED and WILLIAM J. BOWMAN},
journal = {Journal of Functional Programming},
volume = {32},
year = {2022},
doi = {10.1017/s0956796822000090}
}