coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Andrew Appel <appel AT princeton.edu>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Program Logics for Certified Compilers
- Date: Mon, 7 Sep 2020 11:44:02 -0400 (EDT)
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=appel AT princeton.edu; spf=Pass smtp.mailfrom=appel AT cs.princeton.edu; spf=Pass smtp.helo=postmaster AT yellowcard.cs.princeton.edu
- Ironport-phdr: 9a23:BwXIth0swdaSJx/FsmDT+DRfVm0co7zxezQtwd8ZsesWKvXxwZ3uMQTl6Ol3ixeRBMOHsqwC0rCK+PC5EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe8bL9oMRm6swrcusYVjId/N6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhSEaPDA77W7XkNR9gqxbrhy/pBJx3oHbb52UNPR5YqPQZskVSXZdUctLTSFNHoGxYo0SBOQBJ+ZYqIz9qkMSoBu4GAasHv3gyzFVjXLqxa06y/ouEQXb1wEnBd0OqGzUo8vxNKoJSeC11qjIzTPfYPxIxTf9747Ifgo/rv6RQLJ9aMzcwlQgGA3ZlFufs5DlPy+L2eQXtWiW9+ttWP+hhWApqwx8vCaiy9ouh4TKiY8YxVDK+Dh3zog6O9C2R092b9GrHZdNuC+XKoR7TMw+T29otis3xLMLtJ+9cSMXxponwBvfZOaGc4iO+h/jTPyRITZ+hH15Zr2/mxGy8U66xuLiS8a0zU5GoTZfndnJrX8NzR3T5dWISvRj5Euh3iyP1w/V5+pZIk40jbLWJ4M/zrMzjJYfrFnPEjHslEnrgqKbd18o9+mp5uj/f7nrpJGRO5V2hw3jKKgjns2yDf4mPgUAUGWX4fmw2KPg8EHjXblGk+M6nrPEvJ3UJMkXvK60Dg1T340+8RiwFS2m384dnXQfLFJKZhaHj4/xNlDOPv/4CfO/g1OikTh33f/GJKDuDo/RIXjYirvhZax9609ayAUv099f+5VUCrcbLP3tR0DxqcTUDh4/MwOq3+bqEMhx2p0dVG6VH6OVLb3evUWV6u8hIuSAfo4YtTflJ/gg/fHujHs5mVEHfamu2JsacGq3Hux+I0qHZXrhmcsOEXwQsgomVuzqiVuCXiJNaHauWKI84Cs3B5y7AofeXoytmqCO3D+nHp1KYWBLEl+NEXP2eIWeXPcNaDmfI85gkjwBTrehUZUu2QuvtA/80bpnL/Db9jcWtZL5zNJ1/fHclQku9TxoCMSQy32CT2Ztnm8RWzA22L1/rldmx1eY0al4huRYGsZJ6/NIVAc6L5/cwPZgB9D8QAKSNuuOHV2hW5CtBSw7BoY6xMZLaEJgEf2jiArC1mykGelGuaaMAckd9K7G0me5Dt5lxnKOgKA5l1QiatNVNGuti7J48U7eC5OfwBbRrLqjaalJhH2Fz2yE12fb5BgFAj41ar3MWDUkXmWTrdn94RmTHa6jDbAgLQBI08LEIbAMcsfoi15LWPDlftnSfjDowjviNVOz3rqJKbHSVSAFxiyEVRociQEV9nuaMg54Cyu88TqHXW5eUGn3akapytFQ7XayT0s61QaPNh0z3KHz4gQUg/eRV/QVmL8IpXV4pg==
Announcing: free author-page access to
- Program Logics for Certified Compilers, by Andrew W. Appel with Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. Cambridge University Press, 2014.
Our publishing contract allows the authors to make a complete PDF available on the authors' personal web sites. Initially I did not do so, because the publisher's e-book price was less than $15. Now that the e-book price is an unreasonable $72, I am happy to make it available for free.
Some parts of the book have been superseded by more recent work in the Verifiable Software Toolchain. The part that may be most useful is the core explanation of how VST's step-indexed semantic model permits the soundness proof (with respect to the CompCert C semantics) of a higher-order separation logic for a language with function pointers.
Sincerely,
Andrew Appel
Princeton University
- [Coq-Club] Program Logics for Certified Compilers, Andrew Appel, 09/07/2020
Archive powered by MHonArc 2.6.19+.