计算机科学

首页 > 计算机科学

类型论

2018-08-30 10:06:16     所属分类:计算机逻辑

在最广泛的层面上,类型论是关注把实体分类到叫做类型的搜集中的数学和逻辑分支。在这种意义上,它与类型的形而上学概念有关。现代类型论在部分上是响应罗素悖论而发明的,并在伯特兰·罗素和阿弗烈·诺夫·怀海德的《数学原理》中起到重要作用。

在计算机科学分支中的编程语言理论中,类型论提供了设计分析和研究类型系统的形式基础。实际上,很多计算机科学家使用术语“类型论”来称呼对编程语言的类型语言的形式研究,尽管有些人把它限制于对更加抽象的形式化如有类型lambda演算的研究。

目录

  • 1 类型论体系
    • 1.1 主要
    • 1.2 次要
    • 1.3 活跃
  • 2 参考文献
  • 3 延伸阅读
  • 4 外部链接
  • 5 参见

类型论体系

主要

  • 简单类型λ演算,一种高阶逻辑;
  • 直觉类型论;
  • 系统F;
  • LF经常用来定义其他类型论;
  • 构造演算及其派生理论。

次要

  • Automath英语Automath
  • ST类型论;
  • 组合逻辑的一些形式;
  • λ立方体中定义的其他;
  • 其他有类型λ演算;
  • 其他纯类型系统英语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.

外部链接

  • Stanford Encyclopedia of Philosophy: Type Theory" -- by Thierry Coquand.
  • National Institute of Standards and Technology: Abstract data type
  • A summary paper on the formal basis of ADTs, relationship to category theory, and list of good references. Pages 3-4 appear relevant. Reference number 6 looks good, but it may not be available online.
  • Constable, Robert L., 2002, "Naïve Computational Type Theory," in H. Schwichtenberg and R. Steinbruggen (eds.), Proof and System-Reliability: 213-259.
  • The Nuprl Book: "Introduction to Type Theory."

参见

  • 罗素公理体系
  • 直觉类型论
  • 有类型lambda演算
  • 类型系统
  • 域理论
  • 范畴论

上一篇:否定为失败
下一篇:回答集编程
相关推荐