一句话：提出 LRTT 类型理论，以局部抽象封装用户自定义计算规则，并给出保守性证明与 Rocq 原型。
依赖类型理论的证明助手在检查证明时将对象等同于可计算形式，但 Agda、Rocq 等新支持的用户自定义计算规则一旦引入便是全局的，导入相关开发会强制依赖这些规则，可能引发不兼容并破坏终止性、合流性、类型保持与一致性等性质。本文设计 LRTT，在定义层通过前束量化局部抽象用户自定义计算规则，并允许提供一个或多个满足等式定义相等的实例化；同时提出一种类似单态化或 C++ 模板的定义内联过程，以此证明 LRTT 相对于传统 Martin-Löf 类型理论的保守性。作者在 Rocq 证明助手中实现原型并展示示例，且所有结果均已在 Rocq 中形式化。
Proof assistants based on dependent type theory such as Agda, Lean and Rocq identify objects up to computation during proof checking. This takes away some of the proof burden from the user and even provides a way to get very efficient automation. Recently, Agda and Rocq have been extended to support user-defined computation. While they already prove very useful, user-defined computation rules are global : once they are added, they are here to stay. Importing a development that makes use of those rules then means relying on them, whether we want it or not, which can lead to unwanted incompatibilities. We design LRTT, a type theory with support for local abstraction over user-defined computation rules. This takes the form of a prenex quantification at the definition level. This quantification is supplemented with the possibility to provide one or several instantiations that verify the equations definitionally. We show that a procedure inlining definitions abstracting over definitional equality is possible, in the style of monomorphisation or of C++ templates. In the process we get a conservativity result over more conventional Martin-Löf type theories. There are several benefits to such a system. First, it provides encapsulation for user-defined computation rules, which is important to avoid unwanted bad interactions and limits the scope in which invariants of type theory (such as termination, confluence, type preservation and consistency) are broken. Second, abstraction lets users factorise code that crucially relies on definitional equality, as well as hide implementation details that are irrelevant in some settings. Finally, it gives a way to encode certain features without paying the price of the encoding. We showcase such examples in a prototype implementation as an extension of the Rocq Prover. Additionally, all the results in this have been formalised in Rocq.
@article{LerayW26,
title = {Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally},
author = {Yann Leray and Théo Winterhalter},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776704}
}