@inproceedings(SMTLib2010,
 author       = {Clark Barrett and Aaron Stump and Cesare Tinelli},
 year         = {2010},
 title        = {{The SMT-LIB Standard: Version 2.0}},
 editor       = {A. Gupta and D. Kroening},
 booktitle    = {Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK)},
)
@misc(ssrbit,
 author       = {Arthur Blot and Pierre-Evariste Dagand and  and Julia Lawall},
 title        = {Bit Sequences and Bit Sets Library},
 url          = {https://github.com/pedagand/ssrbit},
)
@misc(bbvlib,
 author       = {Tej Chajed and Haogang Chen and Adam Chlipala and Joonwon Choi and Andres Erbsen and Jason Gross and Samuel Gruetter and Frans Kaashoek and Alex Konradi and Gregory Malecha and Duckki Oe and Murali Vijayaraghavan and Nickolai Zeldovich and Daniel Ziegler},
 title        = {Bedrock Bit Vectors Library},
 url          = {https://github.com/mit-plv/bbv},
)
@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. Reasoning},
 volume       = {61},
 number       = {1-4},
 pages        = {423--453},
 doi          = {10.1007/s10817-018-9458-4},
)
@misc(coqbvlib,
 author       = {Jean Duprat},
 title        = {Library Coq.Bool.Bvector},
 url          = {https://coq.inria.fr/library/Coq.Bool.Bvector.html},
)
@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 Barrett},
 year         = {2017},
 title        = {SMTCoq: {A} Plug-In for Integrating {SMT} Solvers into Coq},
 booktitle    = {Proceedings of 29th International Conference on Computer Aided Verification ({CAV} 2017)},
 series       = {Lecture Notes in Computer Science},
 volume       = {10427},
 publisher    = {Springer},
 pages        = {126--133},
 doi          = {10.1007/s10703-012-0163-3},
)
@incollection(ENDERTON200167,
 author       = {Herbert B. Enderton},
 year         = {2001},
 title        = {Chapter TWO - First-Order Logic},
 editor       = {Herbert B. Enderton},
 booktitle    = {A Mathematical Introduction to Logic (Second Edition)},
 edition      = {second edition},
 publisher    = {Academic Press},
 address      = {Boston},
 pages        = {67 -- 181},
 doi          = {10.1016/B978-0-08-049646-7.50008-4},
)
@inproceedings(Gupta:1993:RSM:259794.259827,
 author       = {Aarti Gupta and Allan L. Fisher},
 year         = {1993},
 title        = {Representation and Symbolic Manipulation of Linearly Inductive Boolean Functions},
 booktitle    = {Proceedings of the 1993 IEEE/ACM International Conference on Computer-aided Design},
 series       = {ICCAD '93},
 publisher    = {IEEE Computer Society Press},
 address      = {Los Alamitos, CA, USA},
 pages        = {192--199},
 url          = {http://dl.acm.org.stanford.idm.oclc.org/citation.cfm?id=259794.259827},
)
@inproceedings(DBLP:conf/cav/NiemetzPRBT18,
 author       = {Aina Niemetz and Mathias Preiner and Andrew Reynolds and Clark Barrett and Cesare Tinelli},
 year         = {2018},
 title        = {Solving Quantified Bit-Vectors Using Invertibility Conditions},
 booktitle    = {Proceedings of 30th International Conference on Computer Aided Verification ({CAV} 2018)},
 pages        = {236--255},
 doi          = {10.1007/978-3-319-96142-2\_16},
)
@unpublished(cade2019amaycc,
 author       = {Aina Niemetz and Mathias Preiner and Andrew Reynolds Yoni Zohar and Clark Barrett and Cesare Tinelli},
 year         = {2019},
 title        = {Towards Bit-Width-Independent Proofs in SMT Solvers},
 note         = {To appear in the proceedings of CADE-27},
)
@book(nipkow2002isabelle,
 author       = {Tobias Nipkow and Lawrence C Paulson and Markus Wenzel},
 year         = {2002},
 title        = {Isabelle/HOL: a proof assistant for higher-order logic},
 series       = {Lecture Notes in Computer Science},
 volume       = {2283},
 publisher    = {Springer Science \& Business Media},
 doi          = {10.1007/3-540-45949-9\_6},
)
@inproceedings(DBLP:conf/itp/Sozeau10,
 author       = {Matthieu Sozeau},
 year         = {2010},
 title        = {Equations: {A} Dependent Pattern-Matching Compiler},
 booktitle    = {Proceedings of the 1st International Conference on Interactive Theorem Proving ({ITP} 2010)},
 pages        = {419--434},
 doi          = {10.1007/978-3-642-14052-5\_29},
)
@misc(coqref,
 author       = {The Coq development team},
 year         = {2019},
 title        = {The Coq Proof Assistant Reference Manual Version 8.9},
 url          = {https://coq.inria.fr/distrib/current/refman/},
)