一句话：通过带 quote 算子的 MLTT 扩展，正面证明内部丘奇论题与依赖类型理论兼容，并建立其元理论。
内部丘奇论题（CT）断言任意函数 f : N → N 都可关联到某个图灵完备语言中的具体代码来计算它。CT 在较简单系统中的兼容性早已知道，但与依赖类型理论的兼容性此前仍是开放问题。本文给出肯定回答：定义“MLTT”，即在 MLTT 上加入 quote 算子的类型理论，并在此理论中可导出 CT。作者进一步用标准逻辑关系模型证明该理论一致、强规范化并具有典范性。所有结果均已在 Coq 中机器化验证。
The internal Church thesis (CT) is a logical principle stating that one can associate to any function f : N → N a concrete code, in some Turing-complete language, that computes f. While the compatibility of CT in simpler systems has been long known, its compatibility with dependent type theory is still an open question. In this paper, we answer this question positively. We define "MLTT", a type theory extending MLTT with quote operators in which CT is derivable. We furthermore prove that "MLTT" is consistent, strongly normalizing and enjoys canonicity using a rather standard logical relation model. All the results in this paper have been mechanized in Coq1.