The Software Foundations team is delighted to announce a new release of the entire SF series.
Software Foundations is a set of textbooks on logic, programming language theory, functional algorithms, and machine-assisted proofs of functional and imperative programs, all 100% formalized and machine-checked in Coq. This release brings all volumes up to date with the current release of Coq (8.15.2) and additional tools such as VST and QuickChick.
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. These two volumes have been extensively polished and refined, with many next exercises, improved explanations, and notational improvements – in particular, the concrete syntax of program snippets in examples and proofs is significantly more readable.
Volume 3 (Verified Functional Algorithms) shows how a variety of fundamental data structures can be specified and mechanically verified. The new release features improvements to the sorting and search-tree chapters.
Volume 4 (QuickChick: Property-Based Testing in Coq) introduces tools for combining randomized property-based testing with formal specification and proof in the Coq ecosystem. The new release incorporates recent advances in property-based testing, notably automatic derivation of generators, enumerators, and checkers from inductive relations, plus a discussion of the new pragmas for typeclass instance declarations.
Volume 5 (Verifiable C) is an introduction to verifying C programs with separation logic using the Verified Software Toolchain, with exercises that emphasize data abstraction. New in this release are an additional 10 chapters demonstrating how to use VST’s (relatively) new Verified Software Units for modular verification of modular C programs with API interfaces between the modules.
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. It has been polished throughout.
Share and enjoy!
- Benjamin Pierce and the Software Foundations team