Software Foundations 豆 10.0分
资源最后更新于 2020-07-21 12:53:17
作者：Benjamin C. Pierce
简介· · · · · ·
The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.
The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Coq proof assistant.
The exposition is intended for a broad r...
Logical Foundations is the entry-point to the series. It covers functional programming, basic concepts of logic, computer-assisted theorem proving, and Coq.
Programming Language Foundations surveys the theory of programming languages, including operational semantics, Hoare logic, and static type systems.
Verified Functional Algorithms shows how a variety of fundamental data structures can be specified and mechanically verified.
QuickChick: Property-Based Testing in Coq introduces tools and techniques for combining randomized property-based testing with formal specification and proof in the Coq ecosystem.