Blanchette, Jasmin Christian Automation of Logic, MPI for Informatics, Max Planck Society;
Bentkamp, A., Blanchette, J. C., & Klakow, D. (2017). A Formal Proof of the Expressiveness of Deep Learning. In M. Avala-Rincón, & C. A. Muñoz (Eds.), Interactive Theorem Proving (pp. 46-64). Berlin: Springer. doi:10.1007/978-3-319-66107-0_4.