Program Logics for Certified Compilers [pdf]

Link to announcement about making the book free to access on the authors web pages:

https://sympa.inria.fr/sympa/arc/coq-club/2020-09/msg00016.h...