@manual(ref:Coq:manual,
 author       = {The Coq development team},
 year         = {2004},
 title        = {The Coq proof assistant reference manual},
 organization = {LogiCal Project},
 url          = {http://coq.inria.fr},
 note         = {Version 8.0},
)
@book(ref:NuPRL:book-full,
 author       = {Robert L. Constable and Stuart F. Allen and H. M. Bromley and W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and Scott F. Smith},
 year         = {1986},
 title        = {Implementing Mathematics with the Nuprl Proof Development System},
 publisher    = {Prentice-Hall},
 address      = {NJ},
)
@book(ref:Isabelle:Nipkow:2002:IPA:1791547,
 author       = {Tobias Nipkow and Markus Wenzel and Lawrence C. Paulson},
 year         = {2002},
 title        = {Isabelle/HOL: A Proof Assistant for Higher-order Logic},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/3-540-45949-9},
)
@inproceedings(ref:Agda:Norell:2009:DTP:1481861.1481862,
 author       = {Ulf Norell},
 year         = {2009},
 title        = {Dependently Typed Programming in Agda},
 booktitle    = {Proceedings of the 4th International Workshop on Types in Language Design and Implementation},
 series       = {TLDI '09},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {1--2},
 doi          = {10.1145/1481861.1481862},
)
@article(ref:Idris:JFP:9060502,
 author       = {Edwin Brady},
 year         = {2013},
 title        = {Idris, a general-purpose dependently typed programming language: Design and implementation},
 journal      = {Journal of Functional Programming},
 volume       = {23},
 pages        = {552--593},
 doi          = {10.1017/S095679681300018X},
)
@book(ref:lambda:Bar:84,
 author       = {Henk P. Barendregt},
 year         = {1984},
 title        = {The Lambda Calculus Its Syntax and Semantics},
 edition      = {revised},
 volume       = {103},
 publisher    = {North Holland},
)
@article(DBLP:journals/entcs/Sestoft01,
 author       = {Peter Sestoft},
 year         = {2001},
 title        = {Demonstrating Lambda Calculus Reduction},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {45},
 pages        = {424--432},
 doi          = {10.1016/S1571-0661(04)80973-3},
 note         = {\url{http://www.itu.dk/people/sestoft/lamreduce/}},
)
@techreport(Penn-Lambda-Calculator,
 author       = {Lucas Champollion and Joshua Tauberer and Maribel Romero},
 year         = {2007},
 title        = {{The Penn Lambda Calculator: Pedagogical Software for Natural Language Semantics}},
 type         = {Technical Report},
 institution  = {University of Konstanz, Germany, KOPS},
 url          = {http://kops.ub.uni-konstanz.de/volltexte/2009/9605/},
 note         = {\url{http://lambdacalculator.com/}},
)
@article(ref:TILC:Ruiz:2009:TIL:1594413.1594563,
 author       = {David Ruiz and Mateu Villaret},
 year         = {2009},
 title        = {TILC: The Interactive Lambda-Calculus Tracer},
 journal      = {Electron. Notes Theor. Comput. Sci.},
 volume       = {248},
 pages        = {173--183},
 doi          = {10.1016/j.entcs.2009.07.067},
)
@inproceedings(voronkov:vampire,
 author       = {Alexandre Riazanov and Andrei Voronkov},
 year         = {1999},
 title        = {Vampire},
 booktitle    = {Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings},
 pages        = {292--296},
 doi          = {10.1007/3-540-48660-7_26},
)
@article(schulz:eprover,
 author       = {Stephan Schulz},
 year         = {2002},
 title        = {E - a brainiac theorem prover},
 journal      = {AI Commun.},
 volume       = {15},
 number       = {2,3},
 pages        = {111--126},
)
@inproceedings(korovin:iprover,
 author       = {Konstantin Korovin},
 year         = {2008},
 title        = {{iProver} -- An Instantiation-Based Theorem Prover for First-Order Logic (System Description)},
 editor       = {A. Armando and P. Baumgartner and G. Dowek},
 booktitle    = {Proceedings of the 4th International Joint Conference on Automated Reasoning, ({IJCAR 2008})},
 series       = {Lecture Notes in Computer Science},
 volume       = {5195},
 publisher    = {Springer},
 pages        = {292--298},
 doi          = {10.1007/978-3-540-71070-7_24},
)
@inproceedings(otten:leancop,
 author       = {Jens Otten},
 year         = {2008},
 title        = {leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)},
 booktitle    = {Proceedings of the 4th international joint conference on Automated Reasoning},
 series       = {IJCAR '08},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 pages        = {283--291},
 doi          = {10.1007/978-3-540-71070-7_23},
)
@inproceedings(ref:Sledgehammer,
 author       = {Lawrence C. Paulson and Jasmin C. Blanchette},
 year         = {2012},
 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    = {IWIL 2010. The 8th International Workshop on the Implementation of Logics},
 series       = {EPiC Series in Computing},
 volume       = {2},
 publisher    = {EasyChair},
 pages        = {1--11},
 doi          = {10.29007/36dt},
 url          = {https://easychair.org/publications/paper/wV},
)
@article(sutcliffe:tptp,
 author       = {Geoff Sutcliffe},
 year         = {2009},
 title        = {The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0},
 journal      = {Journal of Automated Reasoning},
 volume       = {43},
 number       = {4},
 pages        = {337--362},
 doi          = {10.1007/s10817-009-9143-8},
)
@inproceedings(hurd:metis,
 author       = {Joe Hurd},
 year         = {2003},
 title        = {First-order proof tactics in higher-order logic theorem provers},
 booktitle    = {Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports},
 pages        = {56--68},
)
@article(robinson:unification,
 author       = {John A. Robinson},
 year         = {1965},
 title        = {A Machine-Oriented Logic Based on the Resolution Principle},
 journal      = {J. ACM},
 volume       = {12},
 number       = {1},
 pages        = {23--41},
 doi          = {10.1145/321250.321253},
)
@article(mm:unification,
 author       = {Alberto Martelli and Ugo Montanari},
 year         = {1982},
 title        = {An Efficient Unification Algorithm},
 journal      = {ACM Trans. Program. Lang. Syst.},
 volume       = {4},
 number       = {2},
 pages        = {258--282},
 doi          = {10.1145/357162.357169},
)
@article(colomb:clauseindexing,
 author       = {Robert M. Colomb},
 year         = {1991},
 title        = {Enhancing unification in PROLOG through clause indexing},
 journal      = {The Journal of Logic Programming},
 volume       = {10},
 number       = {1},
 pages        = {23--44},
 doi          = {10.1016/0743-1066(91)90004-9},
)
@article(gentzen:sequent,
 author       = {Gerhard Gentzen},
 year         = {1935},
 title        = {Untersuchungen {\"u}ber das logische Schlie{\ss}en. I},
 journal      = {Mathematische Zeitschrift},
 volume       = {39},
 number       = {1},
 pages        = {176--210},
 doi          = {10.1007/BF01201353},
)
@inproceedings(benzmueller:leo3,
 author       = {Max Wisniewski and Alexander Steen and Christoph Benzm\"uller},
 year         = {2014},
 title        = {The {Leo-III} Project},
 editor       = {Alexander Bolotov and Manfred Kerber},
 booktitle    = {Joint Automated Reasoning Workshop and Deduktionstreffen},
 pages        = {38},
 url          = {http://christoph-benzmueller.de/papers/W53.pdf},
)