C. Barrett, I. Shikanian, and C. Tinelli, An abstract decision procedure for satisfiability in the theory of inductive data types, J. Satisf. Boolean Model. Comput, vol.3, pp.21-46, 2007.

J. C. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, J. Autom. Reasoning, vol.37, issue.1-2, pp.109-128, 2013.
DOI : 10.1007/BFb0028402

J. C. Blanchette and T. Nipkow, Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder, ITP 2010, pp.131-146, 2010.
DOI : 10.1007/978-3-642-14052-5_11

A. Carayol and C. Morvan, On Rational Trees, CSL 2006, pp.225-239, 2006.
DOI : 10.1007/11874683_15
URL : https://hal.archives-ouvertes.fr/hal-00620171

K. Djelloul, T. Dao, and T. W. Frühwirth, Abstract, Theory and Practice of Logic Programming, vol.2, issue.04, pp.431-489, 2008.
DOI : 10.1007/BF03037057

H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli, DPLL(T): Fast Decision Procedures, CAV 2004, pp.175-188, 2004.
DOI : 10.1007/978-3-540-27813-9_14

D. Jovanovi´cjovanovi´c and C. Barrett, Sharing is caring: Combination of theories, FroCoS 2011, pp.195-210, 2011.

A. Kersani and N. Peltier, Combining Superposition and Induction: A Practical Realization, FroCoS 2013, pp.7-22, 2013.
DOI : 10.1007/978-3-642-40885-4_2
URL : https://hal.archives-ouvertes.fr/hal-00934610

G. Klein, T. Nipkow, and L. Paulson, Archive of Formal Proofs

D. Kozen, Results on the Propositional ??-Calculus, DAIMI Report Series, vol.11, issue.146, pp.333-354, 1983.
DOI : 10.7146/dpb.v11i146.7420

K. R. Leino and M. Moskal, Co-induction simply?Automatic co-inductive proofs in a program verifier, FM 2014, pp.382-398, 2014.

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768

A. Lochbihler, Verifying a Compiler for Java Threads, ESOP 2010, pp.427-447, 2010.
DOI : 10.1007/978-3-642-11957-6_23

A. Lochbihler, Making the java memory model safe, ACM Transactions on Programming Languages and Systems, vol.35, issue.4, pp.1-65, 2014.
DOI : 10.1145/2518191

L. De-moura and N. Bjørner, Efficient E-Matching for SMT Solvers, CADE-21, pp.183-198, 2007.
DOI : 10.1007/978-3-540-73595-3_13

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS 2008, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

G. Nelson and D. C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979.
DOI : 10.1145/357073.357079

T. Pham and M. W. Whalen, RADA: a tool for reasoning about algebraic data types with abstractions, Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013, pp.611-614, 2013.
DOI : 10.1145/2491411.2494597

A. Reynolds and J. C. Blanchette, A decision procedure for (co)datatypes in SMT solvers, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01212585

A. Reynolds and V. Kuncak, Induction for SMT Solvers, VMCAI 2015, pp.80-98, 2014.
DOI : 10.1007/978-3-662-46081-8_5

A. Reynolds, C. Tinelli, A. Goel, S. Krsti´ckrsti´c, M. Deters et al., Quantifier Instantiation Techniques for Finite Model Finding in SMT, CADE-24, pp.377-391, 2013.
DOI : 10.1007/978-3-642-38574-2_26

A. Reynolds, C. Tinelli, and L. De-moura, Finding conflicting instances of quantified formulas in SMT, 2014 Formal Methods in Computer-Aided Design (FMCAD), pp.195-202, 2014.
DOI : 10.1109/FMCAD.2014.6987613

J. J. Rutten, Universal coalgebra: a theory of systems, Theoretical Computer Science, vol.249, issue.1, pp.3-80, 2000.
DOI : 10.1016/S0304-3975(00)00056-6

A. Stump, G. Sutcliffe, and C. Tinelli, StarExec: A Cross-Community Infrastructure for Logic Solving, IJCAR 2014, pp.367-373, 2014.
DOI : 10.1007/978-3-319-08587-6_28

P. Suter, A. S. Köksal, and V. Kuncak, Satisfiability Modulo Recursive Programs, SAS 2011, pp.298-315, 2011.
DOI : 10.1007/978-3-540-77395-5_17

D. Wand, Polymorphic+typeclass superposition, p.2014, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01098078

T. Weber, SAT-Based Finite Model Generation for Higher-Order Logic, 2008.