[TYPES/announce] New release of Software Foundations

[Benjamin Pierce]

The Software Foundations team is delighted to announce a new release
of the entire
SF series <https://softwarefoundations.cis.upenn.edu>.

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 of additional tools such as VST and QuickChick.

Volumes 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20220830/692bf7c9/attachment-0001.htm>