Blanchette, Jasmin Christian Automation of Logic, MPI for Informatics, Max Planck Society;
Blanchette, J. C., & Merz, S. (Eds.). (2016). Interactive Theorem Proving. Berlin: Springer. doi:10.1007/978-3-319-43144-4.