@inproceedings(DBLP:conf/cade/BarbosaROTB19,
 author       = {Haniel Barbosa and Andrew Reynolds and Daniel El Ouraoui and Cesare Tinelli and Clark W. Barrett},
 year         = {2019},
 title        = {Extending {SMT} Solvers to Higher-Order Logic},
 editor       = {Pascal Fontaine},
 booktitle    = {Automated Deduction - {CADE} 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {11716},
 publisher    = {Springer},
 pages        = {35--54},
 doi          = {10.1007/978-3-030-29436-6\_3},
)
@inproceedings(DBLP:conf/types/Besson06,
 author       = {Fr{\'{e}}d{\'{e}}ric Besson},
 year         = {2006},
 title        = {Fast Reflexive Arithmetic Tactics the Linear Case and Beyond},
 editor       = {Thorsten Altenkirch and Conor McBride},
 booktitle    = {Types for Proofs and Programs, International Workshop, {TYPES} 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers},
 series       = {Lecture Notes in Computer Science},
 volume       = {4502},
 publisher    = {Springer},
 pages        = {48--62},
 doi          = {10.1007/978-3-540-74464-1\_4},
)
@article(DBLP:journals/corr/BlanchetteB0S16,
 author       = {Jasmin Christian Blanchette and Sascha B{\"{o}}hme and Andrei Popescu and Nicholas Smallbone},
 year         = {2016},
 title        = {Encoding Monomorphic and Polymorphic Types},
 journal      = {Log. Methods Comput. Sci.},
 volume       = {12},
 number       = {4},
 doi          = {10.2168/LMCS-12(4:13)2016},
)
@inproceedings(DBLP:conf/frocos/BobotP11,
 author       = {Fran{\c{c}}ois Bobot and Andrey Paskevich},
 year         = {2011},
 title        = {Expressing Polymorphic Types in a Many-Sorted Language},
 editor       = {Cesare Tinelli and Sofronie{-}Stokkermans, Viorica},
 booktitle    = {Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbr{\"{u}}cken, Germany, October 5-7, 2011. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {6989},
 publisher    = {Springer},
 pages        = {87--102},
 doi          = {10.1007/978-3-642-24364-6\_7},
)
@inproceedings(DBLP:conf/itp/BohmeW10,
 author       = {Sascha B{\"{o}}hme and Tjark Weber},
 year         = {2010},
 title        = {Fast LCF-Style Proof Reconstruction for {Z3}},
 editor       = {Matt Kaufmann and Lawrence C. Paulson},
 booktitle    = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {6172},
 publisher    = {Springer},
 pages        = {179--194},
 doi          = {10.1007/978-3-642-14052-5\_14},
)
@book(DBLP:books/daglib/0035083,
 author       = {Adam Chlipala},
 year         = {2013},
 title        = {Certified Programming with Dependent Types - {A} Pragmatic Introduction to the Coq Proof Assistant},
 publisher    = {{MIT} Press},
 url          = {http://mitpress.mit.edu/books/certified-programming-dependent-types},
)
@article(DBLP:journals/jar/CzajkaK18,
 author       = {Lukasz Czajka and Cezary Kaliszyk},
 year         = {2018},
 title        = {Hammer for Coq: Automation for Dependent Type Theory},
 journal      = {J. Autom. Reason.},
 volume       = {61},
 number       = {1-4},
 pages        = {423--453},
 doi          = {10.1007/s10817-018-9458-4},
)
@inproceedings(DBLP:conf/lpar/Delahaye00,
 author       = {David Delahaye},
 year         = {2000},
 title        = {A Tactic Language for the System Coq},
 editor       = {Michel Parigot and Andrei Voronkov},
 booktitle    = {Logic for Programming and Automated Reasoning, 7th International Conference, {LPAR} 2000, Reunion Island, France, November 11-12, 2000, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {1955},
 publisher    = {Springer},
 pages        = {85--95},
 doi          = {10.1007/3-540-44404-1\_7},
)
@inproceedings(DBLP:conf/cav/EkiciMTKKRB17,
 author       = {Burak Ekici and Alain Mebsout and Cesare Tinelli and Chantal Keller and Guy Katz and Andrew Reynolds and Clark W. Barrett},
 year         = {2017},
 title        = {SMTCoq: {A} Plug-In for Integrating {SMT} Solvers into Coq},
 editor       = {Rupak Majumdar and Viktor Kuncak},
 booktitle    = {Computer Aided Verification - 29th International Conference, {CAV} 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part {II}},
 series       = {Lecture Notes in Computer Science},
 volume       = {10427},
 publisher    = {Springer},
 pages        = {126--133},
 doi          = {10.1007/978-3-319-63390-9\_7},
)
@inproceedings(DBLP:conf/esop/FilliatreP13,
 author       = {Jean{-}Christophe Filli{\^{a}}tre and Andrei Paskevich},
 year         = {2013},
 title        = {Why3 - Where Programs Meet Provers},
 editor       = {Matthias Felleisen and Philippa Gardner},
 booktitle    = {Programming Languages and Systems - 22nd European Symposium on Programming, {ESOP} 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2013, Rome, Italy, March 16-24, 2013. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7792},
 publisher    = {Springer},
 pages        = {125--128},
 doi          = {10.1007/978-3-642-37036-6\_8},
)
@inproceedings(DBLP:conf/tphol/GregoireM05,
 author       = {Benjamin Gr{\'{e}}goire and Assia Mahboubi},
 year         = {2005},
 title        = {Proving Equalities in a Commutative Ring Done Right in Coq},
 editor       = {Joe Hurd and Thomas F. Melham},
 booktitle    = {Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {3603},
 publisher    = {Springer},
 pages        = {98--113},
 doi          = {10.1007/11541868\_7},
)
@article(Hurd05,
 author       = {J. Hurd},
 year         = {2005},
 title        = {{System Description: The Metis Proof Tactic}},
 journal      = {Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL)},
 pages        = {103--104},
)
@phdthesis(DBLP:phd/hal/Lescuyer11,
 author       = {St{\'{e}}phane Lescuyer},
 year         = {2011},
 title        = {Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq. (Formalisation et developpement d'une tactique reflexive pour la demonstration automatique en coq)},
 school       = {University of Paris-Sud, Orsay, France},
 url          = {https://tel.archives-ouvertes.fr/tel-00713668},
)
@article(DBLP:journals/jucs/Paulson99,
 author       = {Lawrence C. Paulson},
 year         = {1999},
 title        = {A Generic Tableau Prover and its Integration with Isabelle},
 journal      = {J. Univers. Comput. Sci.},
 volume       = {5},
 number       = {3},
 pages        = {73--87},
 doi          = {10.3217/jucs-005-03-0073},
)
@inproceedings(DBLP:conf/lpar/PaulsonB10,
 author       = {Lawrence C. Paulson and Jasmin Christian Blanchette},
 year         = {2010},
 title        = {Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers},
 editor       = {Geoff Sutcliffe and Stephan Schulz and Eugenia Ternovska},
 booktitle    = {The 8th International Workshop on the Implementation of Logics, {IWIL} 2010, Yogyakarta, Indonesia, October 9, 2011},
 series       = {EPiC Series in Computing},
 volume       = {2},
 publisher    = {EasyChair},
 pages        = {1--11},
 url          = {https://easychair.org/publications/paper/wV},
)
@article(pedrot2019ltac2,
 author       = {Pierre-Marie P{\'e}drot},
 year         = {2019},
 title        = {Ltac2: tactical warfare},
 journal      = {CoqPL 2019},
)
@article(DBLP:journals/jar/SozeauABCFKMTW20,
 author       = {Matthieu Sozeau and Abhishek Anand and Simon Boulier and Cyril Cohen and Yannick Forster and Fabian Kunze and Gregory Malecha and Nicolas Tabareau and Th{\'{e}}o Winterhalter},
 year         = {2020},
 title        = {The MetaCoq Project},
 journal      = {J. Autom. Reason.},
 volume       = {64},
 number       = {5},
 pages        = {947--999},
 doi          = {10.1007/s10817-019-09540-0},
)
@inproceedings(DBLP:conf/itp/Tassi19,
 author       = {Enrico Tassi},
 year         = {2019},
 title        = {Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq},
 editor       = {John Harrison and John O'Leary and Andrew Tolmach},
 booktitle    = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}},
 series       = {LIPIcs},
 volume       = {141},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 pages        = {29:1--29:18},
 doi          = {10.4230/LIPIcs.ITP.2019.29},
)