We present the type system $\mathtt{d}$, an extended type system with lambda-typed lambda-expressions. It is related to type systems originating from the Automath project. $\mathtt{d}$ extends existing lambda-typed systems by an existential abstraction operator as well as propositional operators. $\beta$-reduction is extended to also normalize negated expressions using a subset of the laws of classical negation, hence $\mathtt{d}$ is normalizing both proofs and formulas which are handled uniformly as functional expressions. $\mathtt{d}$ is using a reflexive typing axiom for a constant $\tau$ to which no function can be typed. Some properties are shown including confluence, subject reduction, uniqueness of types, strong normalization, and consistency. We illustrate how, when using $\mathtt{d}$, due to its limited logical strength additional axioms must be added both for negation and for the mathematical structures whose deductions are to be formalized. Several appendices deal with extensions and variations of the proposed system.

翻译：我们提出类型系统 $\mathtt{d}$，一种包含Lambda类型Lambda表达式的扩展类型系统。该系统与源于Automath项目的一系列类型系统相关联。$\mathtt{d}$ 通过存在抽象算子及命题算子扩展了现有的Lambda类型系统。$\beta$-归约被扩展以利用经典否定律的一个子集对取非表达式进行规范化，因此$\mathtt{d}$能够统一处理证明和公式，二者均被视作函数表达式。该系统采用自反类型化公理处理常量$\tau$，而任何函数均无法被赋予该常量的类型。我们证明了若干性质，包括合流性、主题归约、类型的唯一性、强规范化及一致性。我们还展示了由于$\mathtt{d}$的逻辑能力有限，在应用时必须为否定及需要形式化推理的数学结构额外添加公理。多个附录讨论了所提出系统的扩展与变体。