程序即证明

Hacker News 读者推荐

…https://www.dropbox.com/s/2umr9ouz0jdelio/1407.pdf?dl=1 * 认知概率模型（Probabilistic Models of Cognition）: https://probmods.org 把逻辑、类型和证明融合在一起的材料，可能还没人写出来。一些不错的入门/先修资料：* 《Program = Proof》: https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching... * 《Concrete Semantics》: http://concrete-semantics.org * 《The Hitchhiker’s Guide to Logical Verification》: https://raw.githubusercontent.com/blanchette/logical_verific...…

nextos 在 HN 的推荐

……每一步想要实现什么，并且用地道的 F# 写出了功能等价的实现。那真的既好玩又有挑战性。第二部分还没碰，我最近正沉迷于塞缪尔·米姆兰（Samuel Mimram）的《Program = Proof》，简直爱不释手，这是我见过的第一本重点讲柯里-霍华德同构（Curry Howard Isomorphism）的书，涵盖了核心逻辑、lambda 演算、类型论和 Agda……太神了。

efvincent 在 HN 的推荐

……多元微积分。分析学在附录中有讨论。所有证明都带有构造性偏向，所以对计算机背景的学生来说非常算法化且自然。习题解答在另一册。* 米姆兰（Mimram）写的《Program = Proof》。讨论了逻辑与计算，带你从基础一路走到依赖类型论（dependent type theory）及更深的内容。使用 OCaml 和 Agda。免费获取地址：https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...

nextos 在 HN 的推荐

找书

豆瓣 微信读书 京东 Open Library

在黑客书架打开完整页面 →

数据整理自 Hacker News 公开评论，数据来源 hackerbooks.org 与 Open Library。