Study note
Software Foundations
Properties
- Type
- Books
- Status
- 想读
- Domain
- Compilers / PL
- Category
- 类型系统、形式化与定理证明
- Source
- book.douban.com
- Vault note
library/books/compilers/Software-Foundations-d4971404da747cd5.md
Summary
可靠软件数学基础系列，用 Coq 证明助手把逻辑基础、程序语言基础和验证函数式算法等内容全部形式化，正文和习题本身就是可机器检查的 proof script。
Highlights
适合从“读懂证明”进入“写出可检查证明”，是学习 Coq、形式化语义和软件验证的核心资料。
Notes
Benjamin C. Pierce；2019-1-9。
Comments
Loading comments...