一句话：确定 DCOI_ω 实例，并证明该依赖不可区分演算逻辑一致、规范化且类型转换可判定。
依赖不可区分演算（DCOI）通过依赖追踪识别无关参数，并在类型转换中利用不可区分性实现证明无关性，以统一机制支持运行时和编译时无关性，还通过带观察者层级的命题等式类型内化不可区分性推理。此前工作只将其作为纯类型系统给出语法类型安全性，尚不清楚是否存在适合作为定理证明类型论的实例。本文确定带无限可预测宇宙层级的 DCOI_ω，证明其逻辑一致、规范化且类型转换可判定，并在 Coq 中机器化验证全部结果。
The Dependent Calculus of Indistinguishability (DCOI) uses dependency tracking to identify irrelevant arguments and uses indistinguishability during type conversion to enable proof irrelevance, supporting run-time and compile-time irrelevance with the same uniform mechanism. DCOI also internalizes reasoning about indistinguishability through the use of a propositional equality type indexed by an observer level. As DCOI is a pure type system, prior work establishes only its syntactic type safety, justifying its use as the basis for a programming language with dependent types. However, it was not clear whether any instance of this system would be suitable for use as a type theory for theorem proving. Here, we identify a suitable instance DCOI ω , which has an infinite predicative universe hierarchy. We show that DCOI ω is logically consistent, normalizing, and that type conversion is decidable. We have mechanized all results using the Coq proof assistant.
@article{LiuCW25,
title = {Consistency of a Dependent Calculus of Indistinguishability},
author = {Yiyun Liu and Jonathan Chan and Stephanie Weirich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704843}
}