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 (not available yet) |
|
QuickChick: Property-Based Testing in Coq introduces tools for combining randomized property-based testing with formal specification and proof in the Coq ecosystem. 
|
| Volume 5 (not available yet) |
|
Verifiable C is an extended hands-on tutorial on specifying and
verifying real-world C programs using the Princeton Verified Software
Toolchain. 
|
| Volume 6 |
|
Separation Logic Foundations is an in-depth
introduction to separation logic—a practical approach to
modular verification of imperative programs—and how
to build program verification
tools on top of it. 
|