一句话：在 Parigot 的 λμ-演算中引入否定类型构造及语法构造，并证明其归约合流、强规范化与主类型性质。
本文研究如何在 Parigot 的 λμ-演算中处理否定。作者提出扩展系统 L，将否定作为类型构造子，并加入否定的引入与消去语法构造；同时扩展归约系统，新增两条归约规则。文章首先证明该归约满足 subject reduction，并借助 Aczel 对 Tait 与 Martin-Löf 平行归约的推广证明其合流性。虽然该类型赋值在表示含蕴涵与否定的自然演绎证明方面存在局限，作者仍证明所有可在该自然演绎系统中证明的命题在 L 中都有见证。最后，利用 Girard 的可归约候选方法证明所有可类型化项都强规范化，并表明 L 的类型赋值具有主类型性质。
We present $\cal L$, an extension of Parigot's $\lambda\mu$-calculus by adding negation as a type constructor, together with syntactic constructs that represent negation introduction and elimination. We will define a notion of reduction that extends $\lambda\mu$'s reduction system with two new reduction rules, and show that the system satisfies subject reduction. Using Aczel's generalisation of Tait and Martin-L\"of's notion of parallel reduction, we show that this extended reduction is confluent. Although the notion of type assignment has its limitations with respect to representation of proofs in natural deduction with implication and negation, we will show that all propositions that can be shown in there have a witness in $\cal L$. Using Girard's approach of reducibility candidates, we show that all typeable terms are strongly normalisable, and conclude the paper by showing that type assignment for $\cal L$ enjoys the principal typing property.