证明与类型
Proofs and types
Jean-Yves Girard · 初版 1989 年
- 14次提及
- 6人推荐
- 10位 HN 评论者
Hacker News 读者推荐
……过去几个月我自己也在研读类型论（type theory）文献（坦白说，更多是从数学角度而不是编程角度），市面上确实很缺优秀的入门资料。吉拉德（Girard）的《Proofs and Types》是一本神作，但读起来并不轻松，而且对程序员来说没有太多直接相关性。如果其他人感兴趣的话（merijnv，我猜这些你都浏览过了），我有……
ionfish 在 HN 的推荐
……Fitting写的《Automated Theorem Proving》是一本不错的教材。就我个人而言，我认为应该从Huth & Ryan入手。逻辑学就是计算机科学（CS）的微积分。然后通过Pierce的《TAPL》或者Girard的《Proofs and Types》这样的书进阶到类型论。接着，根据你的兴趣，你可以继续深入到模型检测（model checking）、程序分析和定理证明。前两个方向的经典著作分别是Katoen以及Nielson & Nielson。
nextos 在 HN 的推荐
哪种资源合适取决于你的背景。如果你喜欢看书，Girard、Lafont和Taylor合著的《Proofs and Types》[1]是一本非常棒的读物，尽管风格很独特。[1] http://www.paultaylor.eu/stable/prot.pdf
mafribe 在 HN 的推荐
找书
数据整理自 Hacker News 公开评论，数据来源 hackerbooks.org 与 Open Library。