[TYPES/announce] New Software Foundations title: Separation Logic Foundations by Arthur Charguéraud

Benjamin Pierce bcpierce at cis.upenn.edu
Wed May 26 08:45:00 EDT 2021


The Software Foundations <https://softwarefoundations.cis.upenn.edu/> team
is pleased to announce another new volume in the series and significant
updates to other volumes.

*NEW!  *Software Foundations volume 6, Separation Logic Foundations
<https://softwarefoundations.cis.upenn.edu/slf-current/index.html>, 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.

[image: image.png]

*UPDATED!*  Volume 2, *Programming Language Foundations*
<https://softwarefoundations.cis.upenn.edu/plf-current/index.html>*,* surveys
the theory of programming languages, including operational semantics, Hoare
logic, and static type systems.  The concrete notations in this volume have
been extensively revamped for better readability, using the advanced
Notation features of recent versions of Coq.

The other volumes in the series have been updated to track the current Coq
release and incorporate many large and small improvements made since the
last release. Watch for a major update to Volume 5, Verifiable C
<http://Watch for a major update to Volume 5, Verifiable C, later this
summer!>, later this summer!

All Software Foundations titles are available electronically, free of
charge.

Share and enjoy!

     - Benjamin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20210526/a75cd0d1/attachment-0001.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image.png
Type: image/png
Size: 131868 bytes
Desc: not available
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20210526/a75cd0d1/attachment-0001.png>


More information about the Types-announce mailing list