一句话：提出 CDLE：仅用纯 lambda 编码、无需辅助数据类型系统的依赖类型演算，并证明其逻辑一致性。
现代构造类型论通常基于纯依赖类型 lambda 演算，并附加用户定义数据类型。本文提出依赖 lambda 消去演算（CDLE），其核心是纯 lambda 编码，不引入辅助数据类型系统。为在 lambda 编码上支持归纳与大消去，作者定义了构造子约束递归类型，以及将简单类型项提升到类型层的 lifting 操作。文章使用格论指称语义为类型建立模型，并据此证明该语言逻辑一致。最后通过若干实例展示 CDLE 的表达能力，并在原型实现 Cedille 中检查这些例子。
Abstract Modern constructive type theory is based on pure dependently typed lambda calculus, augmented with user-defined datatypes. This paper presents an alternative called the Calculus of Dependent Lambda Eliminations, based on pure lambda encodings with no auxiliary datatype system. New typing constructs are defined that enable induction, as well as large eliminations with lambda encodings. These constructs are constructor-constrained recursive types, and a lifting operation to lift simply typed terms to the type level. Using a lattice-theoretic denotational semantics for types, the language is proved logically consistent. The power of CDLE is demonstrated through several examples, which have been checked with a prototype implementation called Cedille.