一句话：提出 System DE，用模式同时追踪终止性与相关性并支持等式反射，使证明可在编译前被擦除。
在允许一般递归的依赖类型函数式语言中，作为证明的程序必须被求值才能保持类型健全性，这迫使程序员在性能与安全性之间取舍。本文提出 System DE：一个显式类型、带模式（mode）的核心演算，支持终止性追踪与等式反射。程序员可以在逻辑子语言中为可能发散的程序书写归纳证明，并将这些证明反射给类型检查器，同时确信编译器会在执行前将其擦除。System DE 的关键设计是用模式同时处理终止性与相关性追踪，这既简化了演算设计，也为未来扩展留出空间。System DE 适合在 Glasgow Haskell Compiler 中使用，也可作为任何通用依赖类型语言的基础。
In dependently-typed functional programming languages that allow general recursion, programs used as proofs must be evaluated to retain type soundness. As a result, programmers must make a trade-off between performance and safety. To address this problem, we propose System DE, an explicitly-typed, moded core calculus that supports termination tracking and equality reflection. Programmers can write inductive proofs about potentially diverging programs in a logical sublanguage and reflect those proofs to the type checker, while knowing that such proofs will be erased by the compiler before execution. A key feature of System DE is its use of modes for both termination and relevance tracking, which not only simplifies the design but also leaves it open for future extension. System DE is suitable for use in the Glasgow Haskell Compiler, but could serve as the basis for any general purpose dependently-typed language.
@article{paperbot1929,
title = {Dependently-Typed Programming with Logical Equality Reflection},
author = {Yiyun Liu and Stephanie Weirich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607852}
}