类型论与形式证明
Type Theory and Formal Proof
Rob Nederpelt, Herman Geuvers · 初版 2014 年
- 15次提及
- 11人推荐
- 13位 HN 评论者
Hacker News 读者推荐
我发现《Type Theory and Formal Proof》的前6章在讲类型论背后的基础数学方面简直太棒了。作者（Nederpelt 和 Geuvers）没有掩盖任何假设，而是一步一步抽丝剥茧。我大学里没学过这些……
codeismath 在 HN 的推荐
……（来自逻辑学家的）其实相当直白，论文在概念上也不见得有多难，主要是抽象层次层层叠叠。顺便提一句，关于这个话题有人向我推荐了 Nederpelt 和 Geuvers 写的《Type Theory and Formal Proof: An Introduction》。我还没机会深入学，但我觉得值得一看。
nicklaf 在 HN 的推荐
书单。我书架上涵盖这些主题的一些书：Simon Thompson 写的《Type Theory and Functional Programming》（搜一下就能找到 PDF）；Rob Nederpelt / Herman Geuvers 写的《Type Theory and Formal Proof》前120页；想看依赖类型（dependent types）早期资料的话（上面那本也有涉及），可以看看 Per Martin-Lof 的《Intuitionistic Type Theory》；还有《Computation and Reasoning: A Type Theory……
codeismath 在 HN 的推荐
找书
数据整理自 Hacker News 公开评论，数据来源 hackerbooks.org 与 Open Library。