Program logics for certified compilers - Appel, Andrew W. (Cambridge Univ. Press, 2014)