类型论体系

主要

简单类型λ演算，一种高阶逻辑；

直觉类型论；

系统F;

LF经常用来定义其他类型论；

构造演算及其派生理论。

次要

Automath （ 英语 ： Automath ） ；

ST类型论;

组合逻辑的一些形式；

λ立方体 （ 英语 ： Lambda cube ） 中定义的其他；

其他有类型λ演算;

其他 纯类型系统 （ 英语 ： pure type system ） 。

活跃

正在研究中的同伦类型论

参考文献

延伸阅读

Andrews, Peter B., 2002. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof , 2nd ed. Kluwer Academic Publishers.

Cardelli, Luca, 1997, "Type Systems," in Allen B. Tucker, ed., The Computer Science and Engineering Handbook . CRC Press: 2208-2236.

Mendelson, Elliot, 1997. Introduction to Mathematical Logic , 4th ed. Chapman & Hall.

Pierce, Benjamin, 2002. Types and Programming Languages . MIT Press. ISBN 0-262-16209-1)

Thompson, Simon, 1991. Type Theory and Functional Programming . Addison-Wesley. ISBN 0-201-41667-0.

Winskel, Glynn, 1993. The Formal Semantics of Programming Languages, An Introduction . MIT Press. ISBN 0-262-23169-7.

参见

罗素公理体系

直觉类型论

有类型lambda演算

类型系统

域理论

范畴论

免责声明：以上内容版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。感谢每一位辛勤著写的作者，感谢每一位的分享。