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 Rocq proof assistant.

The exposition is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers. No specific background in logic or programming languages is assumed, though a degree of mathematical maturity is helpful. A one-semester course can expect to cover Logical Foundations plus most of Programming Language Foundations or Verified Functional Algorithms or Security Foundations, or selections from them.

1. Logical Foundations
2. Programming Language Foundations
3. Verified Functional Algorithms
4. Property-Based Testing in Rocq
5. Verifiable C
6. Separation Logic Foundations
7. Security Foundations

Hosted by the faculty "Computer and Information Science" at the University of Pennsilvania