一句话：提出带完美直觉主义对偶性的简单类型论 DTT，对应单侧极化序列演算，并证明强规范化与类型保持。
论文提出一种新的双直觉主义类型理论——对偶化类型理论（DTT）。DTT 是具有完美直觉主义对偶性的简单类型理论，对应单侧极化序列演算。其逻辑基础是新的命题双直觉主义逻辑 DIL，该逻辑建立在 Pinto 与 Uustalu 的 L 之上，通过删除若干可容许推理规则并采用带极性的对偶化语法来简化推理系统，同时保持一致性与完备性。作者证明 DTT 强规范化与类型保持，并给出 DIL 一致性的直接证明；完备性则通过归约到 L 来证明。
We propose a new bi-intuitionistic type theory called Dualized Type Theory (DTT). It is a simple type theory with perfect intuitionistic duality, and corresponds to a single-sided polarized sequent calculus. We prove DTT strongly normalizing, and prove type preservation. DTT is based on a new propositional bi-intuitionistic logic called Dualized Intuitionistic Logic (DIL) that builds on Pinto and Uustalu's logic L. DIL is a simplification of L by removing several admissible inference rules while maintaining consistency and completeness. Furthermore, DIL is defined using a dualized syntax by labeling formulas and logical connectives with polarities thus reducing the number of inference rules needed to define the logic. We give a direct proof of consistency, but prove completeness by reduction to L.