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 (Verlagsversion)
Blanchette, J. C., Popescu, A., & Traytel, D. (2017). Abstract Soundness. Archive of Formal Proofs.