类型论
类型论体系
主要
简单类型λ演算,一种高阶逻辑;
直觉类型论;
系统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演算
类型系统
域理论
范畴论
免责声明:以上内容版权归原作者所有,如有侵犯您的原创版权请告知,我们将尽快删除相关内容。感谢每一位辛勤著写的作者,感谢每一位的分享。
- 有价值
- 一般般
- 没价值