**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 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 selections
from both.