一句话：提出 GTT：在依赖类型中加入可安全擦除的 ghost 宇宙，并给出一致性证明、擦除与 equality reflection。
论文提出幽灵类型理论（GTT），在依赖类型理论中新增 ghost 数据宇宙。它不像严格命题宇宙那样 proof-irrelevant：ghost 数据可参与证明或排除不可能分支，但运行时能安全擦除；cast 允许用命题相等的值替换 ghost 值，而转换检查可忽略 cast 且保持可靠性。作者给出保持类型的擦除过程，作为程序提取的第一步，并用类似参数性翻译的语法模型证明一致性，从而导出 ghost 代码的 free theorems。GTT 还可扩展支持 equality reflection，并证明无需函数外延性和 identity proof 唯一性即可消除其使用，说明向量长度等归纳索引不影响计算。结果已在 Coq 中形式化。
We introduce ghost type theory (GTT) a dependent type theory extended with a new universe for ghost data that can safely be erased when running a program but which is not proof irrelevant like with a universe of (strict) propositions. Instead, ghost data carry information that can be used in proofs or to discard impossible cases in relevant computations. Casts can be used to replace ghost values by others that are propositionally equal, but crucially these casts can be ignored for conversion without compromising soundness. We provide a type-preserving erasure procedure which gets rid of all ghost data and proofs, a step which may be used as a first step to program extraction. We give a syntactical model of GTT using a program translation akin to the parametricity translation and thus show consistency of the theory. Because it is a parametricity model, it can also be used to derive free theorems about programs using ghost code. We further extend GTT to support equality reflection and show that we can eliminate its use without the need for the usual extra axioms of function extensionality and uniqueness of identity proofs. In particular we validate the intuition that indices of inductive types—such as the length index of vectors—do not matter for computation and can safely be considered modulo theory. The results of the paper have been formalised in Coq.