Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Program Logics for Certified Compilers

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Program Logics for Certified Compilers


Chronological Thread 
  • 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 
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+.

Top of Page