coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] New release of Software Foundations

From: Kevin Sullivan <sullivan.kevinj AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] New release of Software Foundations
Date: Tue, 30 Aug 2022 13:41:36 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=sullivan.kevinj AT gmail.com; spf=Pass smtp.mailfrom=sullivan.kevinj AT gmail.com; spf=None smtp.helo=postmaster AT mail-pj1-f50.google.com
Ironport-data: A9a23:9T++D6zeTossN9no8oV6t+cbwCrEfRIJ4+MujC+fZmUNrF6WrkUOz DZJUGyGb/qMNGXwc4t+Pd7noRwPusfVm4VjTlNor1hgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefQAOCU5NfsYkidfyc9IMsaoU8lyrVRbrJA24DjWVvd4 ouq+aUzBXf8s9JKGjJMg068gEg31BjCkGtwUosWOJinFHeH/5UkJMp3yZOZdxMUcaEIdgKOf Nsv+Znilo/vE7jBPfv++lrzWhVirrc/pmFigFIOM0SpqkAqSiDfTs/XOdJEAXq7hQllkPhK6 +xKlpmgEj4Qfb/WkcgnDjdeNQ9XaPguFL/veRBTsOSWxkzCNmPumrBgURlwMoof9eJ6R2pJ8 JT0KhhXNkHF17/wmuvlDLQ07iggBJGD0Ic3oWxkyTDHBPBgQp3dQqPIzdBd1TY0wMtJGJ4yY uJEMWc/NEicOHWjPH8GBKklk+6UpELZMCNgjFXFoIo9wk3MmVkZPL/FaYKJILRmX/59lUGB4 2nC4m7RGQAfLNXZyDyf83vqiPWnoM/gcIcbFbn97vwzxVPOniocDxoZUVb9qv684qKjZz5BA 3c3wy0NqLhpzXXoXMP0cyfljniikDdJDrK8DNYGwA2Kz6PV5SOQCW4FUiNNZbQaWCkeFWxCO rihz4OBONB/jFGGYSnCqerM/FteLQBQfDBSP3ZVJecQy4C7+Nlbs/7Zcjp0/EeIYjDdHDjxx 3WSrnF7iehLy8EM0Kq/8BbMhDfESnn1ouwdtlS/soGNtFsRiGuZi2qAtwOzARFoct3xc7V5l CJY8/VyFchXZX13qASDQf8WAJai7OufPTvXjDZHRsd/rmv8pC/4JdsPulmSwXuF1O5UKVcFh 2eD6WtsCGN7YRNGkIcsPtzvU5V6pUQePY28B6iFBjaxXnSBXFbfoHsGib+40Gfqn0wh+ZzTy r/KGftA+U0yUPw9pBLvH7l1+eZymkgWmD2OLbimkEzP+eTEOBa9F+xeWHPQNbBR0U9xiF+Km zqpH5DalUs3vSyXSnW/zLP/2nhTcCVjXM+r+pEHHgNBSyI/cFwc5zbq6etJU+RYc259z48kJ 1mxBR1VzkTRn3rCJVnYY3xvcuK9UpN2rHZ9NispZA76138maIepzaEea5pnJel9pLI/laZ5H 6sfZsGNIvVTUTCYqTkQaJ/KqoY9JhmmgAS5OTWoPWokdJl6Sg2VodLpJ1O99CQHAietm9E5p rmsilHSTZYZFlZtCc/XbLSkyFbo5SoRn+d7Xk3pJNhPeRW0oNI6dXCp1vJuepMCMxTOwDeex j26OxZAqLmfuZIx/fnImbuA8NWkHu54KUxQQDvW4LOwAi/FpzbxzIJFVtGISjDTTmbD/quvO LdOxPbmPfxbxVtHvtYuE7tvyq5itdLjq6UAlVZhFXTPKkypU/ZufyHA0s5IualAgLRevFLuC E6I/9BbP5SPOd/kQAFNflt7Nrzb2KFGgCTW4NQ0PF7+uH198o2BXBgAJBKLkiFccOZ4Pd932 +sno8JKuQWzhgBwaYSDhyFQsnyOdzkODv1huZYdD4vmzAEszwgaM5DbDyb35rCJaslNYhZ2e G7K3PKaiuQO3FfGfloyCWPJgbhXi6MItU0Y11QFPVmIxofIi/JfMMe9Ktjrotm5Dymr0t6f/ kBuPkxxYL2MpnJm2ZAFUGerFAVMQhae/yQdDrfPeHLxFyGVuq7ldQXR+tphOGgW9mtden5Q+ 7TwJKPNT2PxZM+otsctcRcNlhEgJOCdMiXNncmmG4KOGJxSjf8JREOxTTJgliYLyv/dSKEKS SeGMQqwhWDG2fYsnpAG
Ironport-hdrordr: A9a23:V7gEBqzYqBNaMb+kx2tHKrPwFb1zdoMgy1knxilNoH1uA7Wlfq WV9sjzuiWE7Qr5NEtQ++xofZPwIk80lqQV3WByB8bHYOCOggLBR72Kr7GD/9SKIVyYygcy79 YHT0G8MrHN5JpB4PoSLDPWLz/o+re6zJw=
Ironport-phdr: A9a23:1Mk5ux8ngIpPef9uWeW2ngc9DxPPW53KNwIYoqAql6hJOvz6uci4Z wqFta4m1QaXFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkelM8NlBYhCsPWQWfyLfrtcjBoV J8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZpO+j5AIHfg9q52uyo5ZHeYAtFiDWgbb9vL Ri9sBncuNQRjYZ+MKg61wHHomFPe+RYxGNoIUyckhPh7cqu/5Bt7jpdtes5+8FPTav1caI4T adFDDs9KGA6+NfrtRjYQgSR4HYXT3gbnQBJAwjB6xH6Q4vxvy7nvedzxCWWIcv7Rq0yVD+/7 alkVQXohT8IOD438m7ZisJ+gqFGrhy/uxNy2JTbbJ2POfdkYq/RYdEXSGxcVchRTSxBBYa8Y pMKAeUfI+ZYro/9rEYToxujAQmsAOLvyiFSiX/wwKY31P8hERzC3AwkHtIOrm7brNPvOKcRT ++10qjIzTPBb/5N1jf97ZLHchElof2WQb1wds/RxFApGgjYgVqetZbrMCmJ1uQRrWeb9exgW Pqzh2I6tQ18rSSjy8Yxh4TUiI8YyVHJ+DhkzYorONC2R1J2bcOkHZZUuS+XNIV7TMM+Tmxot yg3yLkLtJCncCYFzpks2hDRa/uCc4eS4xLjUv6cISpghH17frK/gQy+/la9xe3hUMS/zVVEr jJdn9XSqnwA0wbf58uHR/dn4EutxDeC2xrT5+1YJ00/iLDVJIQ7wrEqk5oeqUTDETHymEXxl KKWc18r+ums6+j+erXmpIKQO5Z6igz+LqgigMO/AeM/MggBW2iU5/6w26Hk/U38WLlKj/s2n bfFsJ3CO8gXuqq0DxVW34sj8RqzESqq3dUCkXQHMF5JYBeHgJLoO1HKLvD4F/C/g1G0nTdw2 vDGOrnhApTTLnfZlrftZ7V95FBCyAoyy9Bf5YlZCr4EIP3pW0/xsMbUAQM+Mwyx2+rnDs5y2 ZsEWW2TGq+ZLL/SsViQ6+4yO+WMfpMauC7hK/g54P7jlWM2mVgEfaWwwZQXbG24Ee99LkWCY Xvsh88BHn0Qsgo/SuzqklyCXiRJa3a8RaJvrg08XYmhFMLIQp2nqL2HxiayWJNMNU5cDVXZM nr2doPMYOoIbCOMK8kpxicZUbygVYYnkxKjqg78yZJoK+PV/msTspe1h4s93PHaiRxnrW88N M+ayWzYFwmc/0sNTj4yhuVkpFBlj02E2u5+iuBZEtpa47VIVB07PNjS1b8yEMj8DyTGeNrBU 1O6WpO+GzhkVc81x94QakA7GNi8jxbB9yWvCr4R0beMAc986brSikD4PN010HPazO8khlgiT NFIMDi9m6p79hbaAcjKnluYkaSCeqEV3SqL/2CGniKVpE8Ndgl2XO3eWGwHIEvbqdOs/kTZU 7qnEqgqKCNEwM+Gb7NIM5jn0A0AS/DkN9DTJWm2ng9cHD6uwbWBJMrvcmQZhmDGDVQc1hoU9 jCAPBQ/ASGopyTfCiZvHBTheRGk9+42s369QkIuqmPCJ0R8y7q4/AIUjv2AWrsS2LwDoiIot zRzGh60wdvXD9OKowcpcr9bZJsx51JO1GSRsAIYXNToNL1mgl8AegIxvE7w1hN1IopFmMku6 ngtyUs6KK6V1k9AayLNxYr5adi1YiH5+BGibbKT20mLio7HvPdSrq5h9RO+5FLMdAJq6Xhs3 thL3mHJ45zLCFBXSpftSgMt8BM8objGYy477oeS1Ht2MKDyvCWRvrBhTOYj1BukeM9Sda2eE wqnWdYHA8yvNuUs3VukcBMCPshd8ac1O4WtcP7Mi8vJdK5w2Smri2hK+tU3yV+I8ytiQ+iO3 Jsbwvea9gSCXjb4ylymt4qk/OIMLSFXFW25xy/+AYdXbaAnZocHB1ClJMivz8l/jZrgM5JB3 GaqHEhOmMqgeB7IKkf4wRUVz0Mc53quhSq/yTVw1TAvtKuWmiLUkazucx8OO2gDQ2cH7x+kO pWwi9EEVU7ubAU3lR2nzUn/zqlf4q94KiHfTFxJcC7/M2x5GvHo5/zSPogVsc1u7H0fWf/ZA xjSUrPnphoGzy7vV3BTwjw2bXDiu5n0mQB7lHPIKX9yqHTDfsQjjRzb5dHaWbtQxm9cHHg+2 WSRXAHieYTxrrD239/Zv+uzVnysTMhWeCjvl8absTejoHdtClu5luyyndvuFU471zX63p9kT 3atzl60b4/12qC9Ke8icFNvAQq28Nd+HoBgm412h5wO2H4YrpqQ9HsD12z0NJ8IvMC2JGpIX jMNz9PPtUL+xUlnL2yAwcT6W2ucxMlJaNyzY2dQ0SU4pZMvau/c/PlPmi17pUC9pATabK1mn zsT/vAp7WYTn+ADvAd+hjXYGL0ZGlNUeDD9jxndpc7rt71ZPSz8FNr4nFo7h92qC6uO5x1RS GqsMIl3Bjd+t41+KA6eiyC1s9C8PoOMMpRL8UfI2xbY07oLdNRrzaFM3HQ/fzq65CxAqaZzj AQyj8/k+tHfcSM1uvr+WEYQNyWpNZ1NvGux3OAOxoDOmNr3VpR5RmdUBt2xEbTxQWhU7bO+Z 2PsWHU9sivJRuaZRFXCrh8g9zWWTdiqLy3FfSFJi4w9G1/NYhQY2llcXS1mzMdmTUbzlZCnK AEhoWlPgzyw4hpUlrAyb0i5AjqZ/V34LG9zEcfXLQIKvFsbuQGIYYrHv7g1R2YBr9WgtFDfc DXFIV4TXCdSAArcQAmyW9vmrc/J9+zSbganB93JZ7jG6elXVvPSgImqzpMj5TGHcMOGInhlC fQ/nEtFR3FwXcrDyX0JTGQMmiTBYtT+xl/08zBrrs257PXgWR7+rYqJBbxINNxz+hewya6dP u+UjSx9JH5WzJQJjXPPzbEe2hYVhUQMP3G1Fq8csCfWUK/KsqpeDhpecyEqccUVt+Qz2Q5CP cOdgdTwl/Z5gvMzF1ZZRAnhl8WuNqloaym2MFLKAlrONazTf2WahZGqJ/nlF/sN1LYx1VX4o zuQHk79My7WkjDoU0rqKuRQlGSBOxcYvoihcxFrAGylTdT8axT9PsUk6F9+ibAymH7OMnYRd DZmdEYY5KaN6SdZnPx5XW9M8HtjL8GLni+Y66/TLZNc4p4JSmxk0vlX5ng30e4f9CZfWPl8g zfftPZrqlCi1/GNk39pDUIIpTFMi4aG+05lPO+Kk/sIEWaB9xUL42KKDh0MrNYwEdzjtZdbz d3Xnb7yIjNPmzo71cQZDsnQbsmANSh4WfIIMDvdDQ9AVTzycG+C3wpSl/ad8nDTpZ8/+MCEc H8mRbpSVVhzHfQfWBwNIQ==
Ironport-sdr: OTd9AFuWRkVKY5+r2UooII/lj/lDOO2Y0AZoNf9gbb9CPo78lTb/GdzjqGOdwaEuLHcWW1kDcd EL0SnV/yFK8bjFe+fXiwALDgEXFrRUA41RScXSb+asdDm5UJljJo4cRG9aAPm2VhZUiABecAWK ZrEjpvT+U5zMtnXZrbYzsd+HYU2166lKASWdv3IUjh33cXEfeNUBahIesF2l7XZKqD+LXY+B23 AeFAb0QEmEVAF+nLxbxE3dRq48GI60BlPHufxObfCkdhdMXHvUx8hWzijtBLHAH/JYBeRYZne4 w9+L2dxqMkVrQe9eyoiLbyYl

Congrats!

On Tue, Aug 30, 2022, 1:25 PM Benjamin Pierce <bcpierce AT cis.upenn.edu> wrote:

The Software Foundations team is delighted to announce a new release of the entire SF series.

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

[Coq-Club] New release of Software Foundations, Benjamin Pierce, 08/30/2022
- Re: [Coq-Club] New release of Software Foundations, Kevin Sullivan, 08/30/2022