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.

翻译：我们提出 $\cal L$，这是对 Parigot 的 $\lambda\mu$-演算的一种扩展，通过添加否定作为类型构造子，以及代表否定引入和消去的语法构造。我们将定义一种归约概念，该概念通过两条新的归约规则扩展了 $\lambda\mu$ 的归约系统，并证明该系统满足主题归约。利用 Aczel 对 Tait 与 Martin-Löf 的并行归约概念的推广，我们证明这种扩展的归约是合流的。尽管类型指派概念在表示涉及蕴涵和否定的自然演绎证明方面有其局限性，我们将证明其中所有可证明的命题在 $\cal L$ 中都有见证项。利用 Girard 的可归约性候选方法，我们证明所有可类型化的项都是强可正规化的，并在论文结尾证明 $\cal L$ 的类型指派具有主类型性质。