Certified Programs and Proofs - Jouannaud, Jean-Pierre; Shao, Zhong (Springer Berlin Heidelberg, 2011)