Logical Foundations, serves as the entry-point to the series. It covers functional programming, basic concepts of logic, computer-assisted theorem proving,and Coq.
Programming Language Foundations, surveys the theory of programming languages, including operational semantics, Hoare logic, and static type systems.
Verified Functional Algorithms, shows how a variety of fundamental data structures can be mechanically verified.
