Blanchette, Jasmin Christian Automation of Logic, MPI for Informatics, Max Planck Society;
https://www.isa-afp.org/browser_info/current/AFP/Abstract_Soundness/document.pdf (Publisher version)
Blanchette, J. C., Popescu, A., & Traytel, D. (2017). Abstract Soundness. Archive of Formal Proofs, 1-15.