C. Barrett, P. Fontaine, and C. Tinelli, The SMT-LIB standard: Version 2.5. Tech. rep, 2015.
DOI : 10.1007/978-3-642-19583-9_2

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.

N. S. Bjørner, Integrating decision procedures for temporal verification, 1998.

J. C. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, Journal of Automated Reasoning, vol.13, issue.5, pp.109-128, 2013.
DOI : 10.1016/B978-044450813-3/50029-1

J. C. Blanchette, J. Hölzl, A. Lochbihler, L. Panny, A. Popescu et al., Truly Modular (Co)datatypes for Isabelle/HOL, ITP 2014, pp.93-110, 2014.
DOI : 10.1007/978-3-319-08970-6_7

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

J. C. Blanchette and A. Paskevich, TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism, CADE-24, pp.414-420, 2013.
DOI : 10.1007/978-3-642-38574-2_29
URL : https://hal.archives-ouvertes.fr/hal-00825086

J. C. Blanchette, A. Popescu, and D. Traytel, Witnessing (Co)datatypes, ESOP 2015, pp.359-382, 2015.
DOI : 10.1007/978-3-662-46669-8_15
URL : https://hal.archives-ouvertes.fr/hal-01212587

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

S. Cruanes, Extending superposition with integer arithmetic, structural induction, and beyond Available at https://who.rocq.inria.fr/Simon, 2015.
DOI : 10.1007/978-3-319-66167-4_10

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.1109/LICS.1988.5132

J. Endrullis, C. Grabmayer, J. W. Klop, and V. Van-oostrom, On equal <mml:math altimg="si1.gif" display="inline" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd"><mml:mi>??</mml:mi></mml:math>-terms, Theoretical Computer Science, vol.412, issue.28, pp.3175-3202, 2011.
DOI : 10.1016/j.tcs.2011.04.011

P. Gammie and A. Lochbihler, The Stern?Brocot tree Archive of Formal Proofs, 2016.

H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli, DPLL(T): Fast Decision Procedures, LNCS, vol.3114, pp.175-188, 2004.
DOI : 10.1007/978-3-540-27813-9_14
URL : ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/GanHNOT-CAV-04.pdf

Y. Ge and L. De-moura, Complete instantiation for quantified formulas in satisfiability modulo theories, CAV '09, pp.306-320, 2009.
DOI : 10.1007/978-3-642-02658-4_25

E. L. Gunter, Why We Can't have SML Style datatype Declarations in HOL, IFIP Transactions, vol.9220, pp.561-568, 1993.
DOI : 10.1016/B978-0-444-89880-7.50042-5

J. Hopcroft, AN n log n ALGORITHM FOR MINIMIZING STATES IN A FINITE AUTOMATON, Theory of Machines and Computations, pp.189-196, 1971.
DOI : 10.1016/B978-0-12-417750-5.50022-1

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
URL : https://doi.org/10.1016/0304-3975(82)90125-6

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/978-3-642-59495-3
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
URL : http://pp.info.uni-karlsruhe.de/uploads/publikationen/lochbihler10esop.pdf

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
URL : http://www.cse.iitb.ac.in/~sangramraje/references/4-NelsonOppen.pdf

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, CADE-25, pp.197-213, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01212585

A. Reynolds, J. C. Blanchette, and C. Tinelli, Model Finding for Recursive Functions in SMT, p.2015, 2015.
DOI : 10.1007/3-540-60675-0_35
URL : https://hal.archives-ouvertes.fr/hal-01242509

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, LNCS, vol.7898, pp.24-377
DOI : 10.1007/978-3-642-38574-2_26
URL : http://www.cs.nyu.edu/~barrett/pubs/RTG+13.pdf

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
URL : http://homepage.cs.uiowa.edu/%7Etinelli/papers/StuST-IJCAR-14.pdf

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
URL : http://lara.epfl.ch/%7Ekuncak/papers/SuterETAL11SatisfiabilityModuloRecursivePrograms.pdf

C. Tinelli and C. G. Zarba, Combining Nonstably Infinite Theories, Journal of Automated Reasoning, vol.290, issue.1, pp.209-238, 2005.
DOI : 10.1007/s10817-005-5204-9

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.