一句话：提出带依赖类型的经典算术相继式演算，以攻克 dPAω 中依赖类型、控制算子、余归纳与惰性共享共存下的正规化难题。
本文研究带依赖类型的经典算术演算，源于 Herbelin 的 dPAω：该演算把可数全称量化的证明编码为分量流，从而由构造性证明导出可数与依赖选择公理，但其正规化与可靠性仅是猜想。主要困难是依赖类型（选择的构造性部分）、控制算子（经典逻辑）、余归纳对象（以流编码 N→A 函数）和带共享的惰性求值同时出现。论文提出一个带依赖类型的相继式演算，试图在同一证明论框架中统一处理这些特征，为 dPAω 的正规化提供基础。摘要未给出实验评估，工作属证明论与类型论元理论研究。
In a recent paper [11], Herbelin developed dPAω, a calculus in which constructive proofs for the axioms of countable and dependent choices could be derived via the encoding of a proof of countable universal quantification as a stream of it components. However, the property of normalization (and therefore the one of soundness) was only conjectured. The difficulty for the proof of normalization is due to the simultaneous presence of dependent types (for the constructive part of the choice), of control operators (for classical logic), of coinductive objects (to encode functions of type N→A into streams (a0, a1, ...)) and of lazy evaluation with sharing (for these coinductive objects).