coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] New release of Software Foundations

From: Benjamin Pierce <bcpierce AT cis.upenn.edu>
To: coq-club AT inria.fr, types-announce AT lists.seas.upenn.edu
Subject: [Coq-Club] New release of Software Foundations
Date: Tue, 30 Aug 2022 13:23:00 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT seas.upenn.edu; spf=None smtp.helo=postmaster AT mail-vs1-f47.google.com
Ironport-data: A9a23:4PPgKKBakOZLrhVW/zblw5YqxClBgxIJ4kV8jS/XYbTApGsn0jBRn 2FKCD3XaKveZjejfYxxOo3n9kIC6pXVzIVlOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yE6j8lkf5KkYAL+EnkZqTRMFWFw0nqPp8Zj2tQy2YjiW1vX0 T/Pi5S31GGNi2Yc3l08sPrrRCNH5JwebxtF1rCWTakjUG72zxH5PrpHTU2CByeQrr1vIwKPb 72rIIdVUY/u10xF5tuNyt4Xe6CRK1LYFVDmZnF+A8BOjvXez8A/+v5TCRYSVatYoxazh/Qsl c5PjsepVgcsErHOtv5BCyANRkmSPYUekFPGCX22sMjW0VafNnWwnLNhC0Y5OYBe8eFyaY1M3 aZAeXZdM1bZ3r3wnO3TpupE3qzPKOHhN5set2trwBnCAP89B43bTqPMo9JUwV/cg+gUR6qCO ZZEMVKDajzfUxBsMWcIIasQhc32vUf1KiJAjFys8P9fD2/7lVQtitABKuH9cduTAM5Rg0ywv XPD522/AxcANdXZxyDtz563rurGnCe+RplLUbPkqbhlh1qcwmFVAxoTPbemnRWnom2EQ/YCd lcWwXE3sqg32FCpYMOhByTt9RZooSUgc9ZXFuQ77iSExazV/xuVCwA4othpOIxOWCgeFWxC6 7OZoz/6LWcw7+DNGBpx4p/R/GziY3FERYMXTXZcFVNt3jX1nG0kYvvyojtLFae0ipjrAmi1z WzV6ic5gLoXgIgA0KDTEbH7b9CE9sehou0dvF2/soeZAuVROtTNi2uAtwOz0Bq4BNzFJmRtR VBd8yRk0MgADIuWiAuGS/gXEbei6p6taWOC2AE+QMh6r2/yoRZPmLy8BhkudC+F1e5UKVfUj LP75Gu9GbcIYSX0Nf4nC25PI51znPCxfTgaahwkRoMWPsIZmP6v8yZpakqdt10BY2B9+ZzTz ayzKJ72ZV5DUfoP5GPvG481jOF2rghjmju7bc6hk3yPj+HFDFbLEudtDbd7RrpmhE9yiF6Fr Yg32grj40k3bdASlQGOrNNLdA9XfCVrbX00wuQOHtO+zsNdMDlJI5fsLXkJIuSJRoxZybXF+ G+TQEhdxAatjHHLM1zWOGtuYaipQI5yq3R9MCAxZA76138maIepzaEea5pqJOl/qbA/laZ5H 6sfZsGNIvVTUTCZqT4TWpnKqtAwfhqcgw/TbTGuZyIyfsI7SgGQoo3kcwLj+TMgFC2yscdi8 bSs2hmCGsgIRh8kEd7bbvTpwl+s5CBPlOV3VkrOA99SZESxqdgydnCt1qc6epheJw/Cyz2W0 xetLS0Z/eSd8ZUo9NTphLyfq9v7GeVJGEcHTXLQ6qy7NHWH82eund1AXeKPcWyPXW/44v/5N +BczvW5LuZe2VgW7MxzFLFkya947Nzq/ucIwgNhFXTNTlKqFrIwfSXcjJcX7vVAlu1DpA+7e kOT4d0Ga7+HD8XoTQwKLw0/Y+XfiPwZxmvI4fIuLBmo7SN75uDcA0BbPh3JljcEabUpb8Uqx uAuvMNQ4Au600J4PtGDhyFS1mKNMn1QDPl9589CWNfm2lgx11VPQZ3AESuqspuBXNNBbxsxK TiOiaue2rlRyyIuqZbo+aQhAAacuXgPhPyO5FoLJlDMhMGcw/Frg1te9jM4SgkTxRJCuw621 q6HKGUtTZhiPR8x7CSAY4xoMxpMDQbf51T8zV1PmWHEJ6VtfnKYN3UzYI5h42hAm1+xvVFnE HWww2f+Fyvyccf3mCY+RCaJbhAlocNZrmX/pSxsIyhJ81TWr9Yobm9CqFfkcyfaPP4=
Ironport-hdrordr: A9a23:mAjXXKD/T6K/+vnlHemJ55DYdb4zR+YMi2TDj3oBLiC8cqSj+P xG785rsyMc6QxhJU3I9urwW5VoLUmwyXcx2/h0AV7AZnibhILLFvAB0WKK+VSJcEfDH6xmpM JdmsNFZuEYeGIbsS+M2miF+rgbrOVvu5rY/Ns2h00dNT2DfclbnnxE4yigYzdLeDU=
Ironport-phdr: A9a23:HiKzbhEfluSLby3eEwd1751Gf/FGhN3EVzX9CrIZgr5DOp6u447ld BSGo6k31xmTDd6Qsqsew8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PdbglSmjawYr1/I BqroQnMqMUdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3U bJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5 LptRRT1iikIKiQ5/XnYhcJwgqxVow+vqQJjzIPPeo6ZKOBzc7nBcd8GR2dMWNtaWSxbAoO7a osCF/cMMvher4n/vVQOqBq+BQ+xD+31yz9HmGX20rEk3O88FgzJxxAvH8oPsHvKttX6KLkdX Pupw6nJ1jXPde5W2S/j54jOdBAtu++DUq9tccfIz0QkCgzKgEmKp4P/IzOVyvoCs3Kd7+d4S O6ihG4ppx1trzWg2MoglpXFi4ILx13K8Sh0w4g4K9K4RUJnf9OpEYZcuj+VOYZ3Qs0vQWNlt iY7x7EYp5K2fy4Hw4kpyR7YbvyIaYmI4hT7WeaMOTd3mnRleLSlixms7Eeg1+vxXdS33lZSt idJjMXAu3QX2xHQ6sWLUOVx8lqj1DqV2A3e6OdJKl0um6XBMZ4u2Lswm4ITsUvdGi/2n137j KqMeUUl/uik8vrnYq77qpOFOY95hQPzPr4hmsy4BuQ4PQwOUHaB9eug073j+FX1QLRMjvIoj qnUqI7WKdgfq6KjAAJY0pwv5wiiAzqkytgVknsKIEpAeB2djojpP1/OIOr/Dfe6m1mjiytkx +jHPrL/GJXCMmbMnaz6fblj8UFc0xA/zc1H551KDLEBJuj/VVHsu9zFFhM5NRe7zP79CNphz oMeRX6PAqiBPa/PqVOI/P4gI/GQZI8JvzbwM+Qq5/n3jXMghVAdebSp0oAMZXCjHvVmJl2Zb mD2jtcAF2cKpAs+Q/bwhF2MSz4AL0q1Cqk7/3QwDJ+sJYbFXIGkxrKbmG+nD4VbfSVPDFaLD HHjeq2AWuwQc2SJL8Z61CEcWL6nDYItyEKArgj/npBqKOjd/ywe/ari2cJ+6qWHnxoq9DFuB Mm12GCWCXxsk2UOATI6wfYs8gRG1l6f3P0g0LRjHttJ6qYROu9bHZvVzughTsv3RhqEZdCRD lCvXtShBzg1CNM32d4HJUhnSJ25lh6W+S2sDvcOkqCTQoQu+/fW1GDwKtx2xl7N1bJnkkErR M0JOGG71eZk7waGP4fSiA2CkrqyM6EV3SrD7mCGmGCFpEBVSgV9eb7IVGtZe1Pbq9K/60/fH Pe1EbpyFAxHxIaZL7dSLN3kiVITXPD4JNHXeH68gU+1DBeMg62XNc/kJzpb0yLaB0wJ1QsU+ B5qLCAYASGs6yLbBT1qThf0Zl/0tPJ5sDW9R1M1yAeDawtg0aC081gbn67UTfRbxb8CtCo7z lc8VF+gw9LbDcaBrAt9be1dZ906+lJOyWPesUR0IJWhK6loglNWfR5wugvi0BB+C4MIlsZPz jtixgFqKK+C215pfDKDm43oN7vRbGT+4VHnaqLb3E3fzMfD4r0Gu5Fa4x3ouACkEFZn8m0yi YEElSvBoM+TU0xODsGUMA5/7RVxqrDEbzNo4orV0SYpKqyoqnrZ3MpvAuI5yxGmdtMZMaWeF Qa0HddJYqrmYOEshVWtaQoJee5I86thdcmtb/qLwqWmFP1tlSngkHxK5oY7306RvXkZKKaAz 9MezveU0xHSHT33lFasqMv6sYtFfncPBme5z27pCJMbNcgQNc4bTGypJcOw3NB3gZXgDmVZ+ FCUDFQDwMa1eBCWYjQRxCVo3F8M6TyikCq8lHlvli0x67GYxGrIyvjjcxwOPihKQnNjhBHiO 9r8g9cfVUmuJw8n8XntrUzx36lWvq9yB3LeSFwOYjD7KWckX6et/raPeM9A7po0vD4fCrztJ wDHDOSk/F1GjGvqBCNGySo+di22t5mc/VQyk2+bIHtp7TLYdcx22RbD9YnZTP9V0CABQXowg j3WC16getixqI/MxtGT76bkDj3nCsIAFEujhZmNvya6+2BwVBi2nvTo38biDRB/yijjkd9jS STPqh/4JIjtzaWzd+x9LSwKTBfx7dR3HoZmn84+npYVjDIQjY2U8GAMnE/oPNxAn7/mYXwLA zMH3pSGhWqtkF0mNX+Py4/jAz+XydNgasOxb0sN1ysmqd1SBaGSqrFIgGEmxzjw5RKUav97k DAHzPIo43NPmOAFtj0mySCFC6wTF01VbmT80g6F5NekoOBLdX6iJPKugVFmk4nrX9Tg6klMH Wz0cZA4EWps49VjZRjShWbr5NisecGMP4lO8ETFy1Ga07cTcNVryrILnXY1Zz675yZ+jbdl1 Vo2msjr2erPY2R1oPDnXFgBbmezP4VLvWu1xadGwpTIgcb1QsQnSm1NBNyyFbqpCG5A6q6hb lrISWxm7C/cQOq6f0fX6V86/S2TVcnxajfPYiFelIsqRQHBdhUH0EZNA2p8zthhUVrzjM35L BUguWtXvw+k7EMKkqUxaXydGi/evFv6MG9lDsjCakMMvkcaoB6Kec2GsrApRn8eo83n9V3Xb DTcPlUADHlVCBbdWRa5ZejovoOGq6/BV4/cZ7PYaLGK44SyTt+uwpSimstj9jeIbYCUO2V6S uY8wgxFVGx4HMLQn3MOTTYWnmTDdZzTohD04SBxos2llZajEAvy+YuCDadTOtRz6li3h6mEL euZmCd+L35RyJoNwXbCzLVX0kQVjmlicDykELJIsiCoLuqYgqhMExsScD9+LuNN5qM4mxdWY IvV1oyz2bl/gfo4TVxCUB2pm82kY9ALP3DoNF7DAxXuVvzOLjnKzsfrJKKkHOcI3aME6lvq4 GndTxCwW1bL3yPkXB2uL+xW2SSSPRgF/Zq4bg4oEm/7CtTvdhy8NtZzyzww27w9wH3QZgt+e XBxdV1AqrqI4GZWmPJ6TiZL5WJkIPOPlg6C4uDDbIsOvP1tRCl4iqgJhRZyg6sQ9yxCSPFvz WHKqcVypli9juSV4j9uUR4LtC0SwYzX4gNtPqLW8pQGUnHBtkFojy3YG1EBoN1rDcfqsqZbx 43Ula79HzxF9srd4coWA8W8wCOvNXMgNV/3A2eRAldaCzGsMm7bigpWl/TArhV9S7Axq4Oqh YIDTLkdWVAoRKty4qtNB9ELO9FqRj4il/iWgNNavBKD
Ironport-sdr: 8FpX8Ml6xot7lYIXn4jtL4Rwzw05M8tAsdx1fUd/Kc+eTvyXGk+Y7BQ/0nSthZFRtic75i/5Up FHe2I18FbjMsKh+dTv601HSuw44HztPzshcCsgWzGAaM29Kx3nfB82fWKN4HWpbGUSG2Tv9XKH 36r4+slqN9I9K5giQ4uenrnEkbYvMBkAPan9/w+OteLUoY/Szv+D2qcOUQJTZNlN97xYRkyGnz OCryCnF/uWMBhEkb7hy3rN1hKYdIP67Du2o5vv08jYOkRPSSvj8iq75XJ4TVetTyy5vxViNE1/ wiuXWq4DqvcLRNmbJ7gV9kdI

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