Blanchette, Jasmin Christian Automation of Logic, MPI for Informatics, Max Planck Society;
Reynolds, A., & Blanchette, J. C. (2015). A Decision Procedure for (Co)datatypes in SMT Solvers. In A. P. Felty, & A. Middeldorp (Eds.), Automated Deduction -- CADE-25 (pp. 197-213). Berlin: Springer. doi:10.1007/978-3-319-21401-6_13.