一句话：提出扩展类型系统 d，以 λ 类型化 λ 表达式统一处理证明与公式，并证明其归一化与一致性。
本文提出系统 d，一个带 λ 类型化 λ 表达式的扩展类型系统，源自 Automath 传统。它在既有 λ 类型系统中加入存在抽象算子与命题算子，并扩展 β-归约，使其依据部分经典否定律也能归一化被否定的表达式，从而将证明与公式统一视为函数表达式。系统 d 采用常元 τ 的自反类型公理，且任何函数都不能赋予 τ 类型。作者证明合流性、主体归约、类型唯一性、强归一化与一致性。由于系统逻辑强度有限，文中还说明在使用 d 形式化数学结构时，需要分别针对否定和待形式化结构添加额外公理。
We present the 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 type 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.Comment: for extended version, see arXiv:1803.06488
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1803-10143,
title = {An extended type system with lambda-typed lambda-expressions},
author = {Matthias Weber},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 4},
year = {2020},
doi = {10.23638/lmcs-16(4:12)2020}
}