一句话：提出 λert 类型理论，让程序员显式嵌入精化性质的证明，从而支持量词和归纳，并用 Lean 4 证明其可靠性。
精化类型传统上通过 SMT 求解器自动检查，如 DML 与 Liquid Haskell，但受限于可判定片段，难以表达量词和归纳等丰富性质。本文提出 λert：一种支持显式证明的精化类型理论，要求并允许程序员在程序文本中嵌入性质证明，从而将验证负担从 SMT 求解转移到显式证明项。作者证明类型系统可靠：任何精化程序擦除后都是简单类型程序；再借助指称语义证明擦除后的程序满足其精化类型所要求的全部性质。所有证明均在 Lean 4 中机器化验证。该工作展示了在依赖 SMT 的自动化路线之外，如何通过显式证明支持更丰富的逻辑性质。
We present λ ert , a type theory supporting refinement types with <em>explicit proofs</em>. Instead of solving refinement constraints with an SMT solver like DML and Liquid Haskell, our system requires and permits programmers to embed proofs of properties within the program text, letting us support a rich logic of properties including quantifiers and induction. We show that the type system is sound by showing that every refined program erases to a simply-typed program, and by means of a denotational semantics, we show that every erased program has all of the properties demanded by its refined type. All of our proofs are formalised in Lean 4.