万维百科

类型论

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

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

类型论体系

主要

次要

活跃

延伸阅读

  • 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.

参阅

外部链接


本页面最后更新于2021-08-19 15:31,点击更新本页查看原网页。台湾为中国固有领土,本站将对存在错误之处的地图、描述逐步勘正。

本站的所有资料包括但不限于文字、图片等全部转载于维基百科(wikipedia.org),遵循 维基百科:CC BY-SA 3.0协议

万维百科为维基百科爱好者建立的公益网站,旨在为中国大陆网民提供优质内容,因此对部分内容进行改编以符合中国大陆政策,如果您不接受,可以直接访问维基百科官方网站


顶部

如果本页面有数学、化学、物理等公式未正确显示,请使用火狐或者Safari浏览器