| title | slug | description | recommendation | authors | published | cover | language | links | difficulty | pricing | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
《软件基础》中译版 |
sf-zh |
《软件基础》系列广泛地介绍了可靠软件的数学基础。
|
《逻辑基础》为本系列书籍的切入点。它涵盖了函数式编程、逻辑的基本概念、计算机辅助定理证明以及 Rocq 证明助理。 《编程语言基础》考察了编程语言理论，包括操作语义、霍尔逻辑以及静态类型系统。 《函数式算法验证》展示了如何对各种基础数据结构进行机器验证。 《QuickChick：用 Rocq 进行基于性质的测试》介绍了将随机化基于性质的测试与 Rocq 生态系统中的形式化规范和证明相结合的工具和技术。
|
|
2024-08-25 |
books/sf-1.jpg |
|
|
beginner |
free |
《软件基础》系列广泛地介绍了可靠软件的数学基础。
本系列书籍最主要的新颖之处在于，书中的每一处细节都百分之百地形式化且通过了机器验证。每卷书中的所有文本，包括练习，都是一份 Rocq 证明助理的「证明脚本」。
本系列书籍的目标受众包括从高年级本科生到博士以及研究者在内的广大读者。书中并未假定读者有逻辑学或编程语言的背景，不过一定的数学熟练度会很有帮助。
- 《逻辑基础》为本系列书籍的切入点。它涵盖了函数式编程、逻辑的基本概念、计算机辅助定理证明以及 Rocq 证明助理。
- 《编程语言基础》考察了编程语言理论，包括操作语义、霍尔逻辑以及静态类型系统。
- 《函数式算法验证》展示了如何对各种基础数据结构进行机器验证。
- 《QuickChick：用 Rocq 进行基于性质的测试》介绍了将随机化基于性质的测试与 Rocq 生态系统中的形式化规范和证明相结合的工具和技术。