一句话：提出依赖不可区分性演算 DCOI，把不可区分性内化为类型检查器相等性与观察者索引命题相等类型。
在带依赖跟踪的类型系统中，程序员可为计算标注层级以阻止信息从高层流向低层，其核心是不可区分性：一种考虑观察者可依赖程序哪些部分的程序等价。本文研究依赖类型语言中的依赖跟踪，提出依赖不可区分性演算 DCOI。DCOI 将不可区分性作为类型检查器使用的相等性定义，并把它内化为观察者索引的命题相等类型，使程序员能在语言内推理不可区分性。该设计推广并扩展了先前结合依赖跟踪与依赖类型的系统，首次支持任意观察者层级上的转换（conversion）和命题相等。作者证明了 DCOI 的类型可靠性与非干涉定理，并实现了类型检查器原型。
In type systems with dependency tracking, programmers can assign an ordered set of levels to computations and prevent information flow from high-level computations to the low-level ones. The key notion in such systems is indistinguishability : a definition of program equivalence that takes into account the parts of the program that an observer may depend on. In this paper, we investigate the use of dependency tracking in the context of dependently-typed languages. We present the Dependent Calculus of Indistinguishability (DCOI), a system that adopts indistinguishability as the definition of equality used by the type checker. DCOI also internalizes that relation as an observer-indexed propositional equality type, so that programmers may reason about indistinguishability within the language. Our design generalizes and extends prior systems that combine dependency tracking with dependent types and is the first to support conversion and propositional equality at arbitrary observer levels. We have proven type soundness and noninterference theorems for DCOI and have developed a prototype implementation of its type checker.
@article{paperbot2628,
title = {Internalizing Indistinguishability with Dependent Types},
author = {Yiyun Liu and Jonathan Chan and Jessica Shi and Stephanie Weirich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632886}
}