[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
To accompany the new Security Foundations volume, the Software Foundations
team is *also *pleased to announce a new major release of all six existing
volumes
<https://urldefense.com/v3/__http://softwarefoundations.org__;!!IBzWLUs!SK88hH7G3ngERHdAgA1_-klG-yHQgVL7XgtvjxaWvr7whX5vRU7rCfIpyEprsfw6XCZT6mXpOPRyccVFUHlUK3xRfeRHiP7lcBZW$
>:
- *Logical Foundations*,
*by Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco
Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, and Brent
Yorgey, *is the entry-point to the series. It covers functional
programming, basic concepts of logic, computer-assisted theorem proving,
and Coq.
- *Programming Language Foundations, by Benjamin C. Pierce, Arthur
Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael
Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent
Yorgey, *surveys the theory of programming languages, including
operational semantics, Hoare logic, and static type systems.
- *Verified Functional Algorithms, by Andrew W. Appel,* shows how a
variety of fundamental data structures can be specified and mechanically
verified.
- *QuickChick: Property-Based Testing in Coq, by Leonidas Lampropoulos
and Benjamin C. Pierce,* introduces tools for combining randomized
property-based testing with formal specification and proof in the Coq
ecosystem.
- *Verifiable C, **by* *Andrew W. Appel, Lennart Beringer, and Qinxiang
Cao**, *is an extended hands-on tutorial on specifying and verifying
real-world C programs using the Princeton Verified Software Toolchain.
- *Separation Logic Foundations, by Arthur Charguéraud*, 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.
- And now... *Security Foundations, by Cătălin Hriţcu and Yonghyun Kim*,
studies the security of programs by setting clear and rigorous security
goals and developing provable enforcement mechanisms.
The new release incorporates numerous improvements, extensions, and reader
contributions -- in particular, it is compatible with Rocq 9.0.
Share and enjoy,
- Benjamin Pierce
(SF series editor)
