简单类型论的一种形式化（用于 Isabelle）
计算机科学中的逻辑
2008-02-03 v1
摘要
为了与通用定理证明器 Isabelle 配合使用，对简单类型论进行了形式化。这需要显式的类型推理规则。其中有函数类型、积类型和子集类型，它们可以为空。描述（eta 算子）引入了选择公理。通过公式与 bool 类型项之间的反射获得了高阶逻辑。递归类型和函数可以被形式化地构造。描述了 Isabelle 的证明过程。该逻辑似乎适用于一般数学以及计算问题。
引用
@article{arxiv.cs/9301107,
title = {A Formulation of the Simple Theory of Types (for Isabelle)},
author = {Lawrence C. Paulson},
journal= {arXiv preprint arXiv:cs/9301107},
year = {2008}
}