依赖类型认证编程
Certified Programming with Dependent Types
Adam Chlipala · 初版 2013 年
- 26次提及
- 15人推荐
- 23位 HN 评论者
为什么值得读
指导在Coq中使用依赖类型与自动化脚本编程
- 讲解利用依赖类型构建带正确性证明的程序
- 着重介绍实用的证明自动化工具与工程实践
- 适合作为掌握Coq基础之后的进阶挑战教材
适合：想深入学习Coq自动化证明与验证工程的开发者
值得读指数：78 / 100
Hacker News 读者推荐
……用起来相当痛苦。一旦我真正需要形式化验证过的代码，用 Coq 似乎是最省事的一条路，因为它的自动化证明工具链相当赞，特别是如果你按照《Certified Programming with Dependent Types》[0]里的思路来做的话。我也挺喜欢用 Alloy[1] 来交互式折腾逻辑数据结构的定义。[0] http://adam.chlipala.net/cpdt/ [1] http://alloy.mit.edu/alloy/
erichocean 在 HN 的推荐
如果你想入门 Coq，有两个很棒的资源。一个是 Benjamin Pierce 写的《软件基础》（Software Foundations，[sf]）。还有一本是 Adam Chlipala 写的《Certified Programming with Dependent Types》（[cpdt]）。我觉得 [cpdt] 比 [sf] 更加进阶，所以最好先从 [sf] 看起，要是觉得自己准备好迎接挑战了，再啃 [cpdt]。我对 Coq 的心情很复杂……
reycharles 在 HN 的推荐
想要学这方面的内容，我一向推荐 Pierce 的《Software Foundations》[0] 和 Chlipala 的《Certified Programming with Dependent Types》[1]，这两本网上都有免费版。不过我也在看《Coq d'Art》，非常喜欢……可惜这本书不太好找。[0] http://www.cis.upenn.edu/~bcpierce/sf/current/index.html…
tel 在 HN 的推荐
找书
数据整理自 Hacker News 公开评论，数据来源 hackerbooks.org 与 Open Library。