Welcome to the jsCoq-powered version of Software Foundations.
This version contains the same text and code from the beloved Software Foundations series. All the code in the book is executable and can be run directly on the page while reading the book. Look for the jsCoq icon on the top right corner of each page.
| Volume 1 |
|
Logical Foundations is the entry-point to the series. It covers functional programming, basic concepts of logic, computer-assisted theorem proving, and Coq. 
|
| Volume 2 |
|
Programming Language Foundations surveys the theory of programming languages, including operational semantics, Hoare logic, and static type systems. 
|
| Volume 3 |
|
Verified Functional Algorithms shows how a variety of fundamental data structures can be specified and mechanically verified. 
|
| Volume 4 |
|
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. 
|