类型论概览
逻辑
2014-11-07 v2
摘要
纯类型系统作为简单类型 lambda 演算的推广而出现。数学的当代发展重新激发了人们对类型论的兴趣，因为它们不仅是纯粹历史研究的对象，而且在计算科学和核心数学的发展中发挥着积极作用。值得深入探索其中的一些理论，特别是谓词的 Martin-L"of 直觉主义类型论和非谓词的 Coquand 构造演算。本文将研究它们之间的逻辑和哲学异同，并展示这些类型论与其他逻辑领域之间的关系。
引用
@article{arxiv.1411.1029,
title = {An overview of type theories},
author = {Nino Guallart},
journal= {arXiv preprint arXiv:1411.1029},
year = {2014}
}
备注
Conference: Philosophy of Science in the 21st Century: Challenges and Tasks, Faculdade de Ci\^encias da Universidade de Lisboa (Portugal), December 2013