@article(baelde12tocl,
 author       = {David Baelde},
 year         = {2012},
 title        = {Least and greatest fixed points in linear logic},
 journal      = {ACM Trans.\ on Computational Logic},
 volume       = {13},
 number       = {1},
 doi          = {10.1145/2071368.2071370},
 url          = {http://tocl.acm.org/accepted/427baelde.pdf},
)
@article(baelde14jfr,
 author       = {David Baelde and Kaustuv Chaudhuri and Andrew Gacek and Dale Miller and Gopalan Nadathur and Alwen Tiu and Yuting Wang},
 year         = {2014},
 title        = {Abella: {A} System for Reasoning about Relational Specifications},
 journal      = {Journal of Formalized Reasoning},
 volume       = {7},
 number       = {2},
 doi          = {10.6092/issn.1972-5787/4650},
 url          = {http://jfr.unibo.it/article/download/4650/4137},
)
@inproceedings(baelde07lpar,
 author       = {David Baelde and Dale Miller},
 year         = {2007},
 title        = {Least and greatest fixed points in linear logic},
 editor       = {N. Dershowitz and A. Voronkov},
 booktitle    = {International Conference on Logic for Programming and Automated Reasoning (LPAR)},
 series       = {LNCS},
 volume       = {4790},
 pages        = {92--106},
 url          = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lpar07final.pdf},
)
@inproceedings(baelde10ijcar,
 author       = {David Baelde and Dale Miller and Zachary Snow},
 year         = {2010},
 title        = {Focused Inductive Theorem Proving},
 editor       = {J. Giesl and R. H{\"a}hnle},
 booktitle    = {Fifth International Joint Conference on Automated Reasoning},
 series       = {LNCS},
 volume       = {6173},
 pages        = {278--292},
 doi          = {10.1007/978-3-642-14203-1\_24},
 url          = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ijcar10.pdf},
)
@misc(Bedwyr,
 year         = {2015},
 title        = {The {B}edwyr system},
 note         = {Available at \url{http://slimmer.gforge.inria.fr/bedwyr/}},
)
@book(boyer79,
 author       = {Robert S. Boyer and J. Strother Moore},
 year         = {1979},
 title        = {A Computational Logic},
 publisher    = {Academic Press},
)
@article(bundy93ai,
 author       = {A. Bundy and A. Stevens and F. van Harmelen and A. Ireland and A. Smaill},
 year         = {1993},
 title        = {Rippling: {A} Heuristic for Guiding Inductive Proofs},
 journal      = {Artificial Intelligence},
 volume       = {62},
 number       = {2},
 pages        = {185--253},
 doi          = {10.1016/0004-3702(93)90079-Q},
)
@inproceedings(bundy87cade,
 author       = {Alan Bundy},
 year         = {1987},
 title        = {The use of explicit plans to guide inductive proofs},
 booktitle    = {Conf. on Automated Deduction (CADE 9)},
 pages        = {111--120},
)
@inproceedings(chihani13cade,
 author       = {Zakaria Chihani and Dale Miller and Fabien Renaud},
 year         = {2013},
 title        = {Foundational proof certificates in first-order logic},
 editor       = {Maria Paola Bonacina},
 booktitle    = {CADE 24: Conference on Automated Deduction 2013},
 series       = {LNAI},
 volume       = {7898},
 pages        = {162--177},
 doi          = {10.1007/978-3-642-38574-2\_11},
)
@book(miller12proghol,
 author       = {Dale Miller and Gopalan Nadathur},
 year         = {2012},
 title        = {Programming with Higher-Order Logic},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139021326},
)
@inproceedings(pfenning99cade,
 author       = {Frank Pfenning and Carsten Sch{\"u}rmann},
 year         = {1999},
 title        = {System Description: Twelf --- {A} Meta-Logical Framework for Deductive Systems},
 editor       = {H. Ganzinger},
 booktitle    = {16th Conf.\ on Automated Deduction (CADE)},
 series       = {LNAI},
 volume       = {1632},
 publisher    = {Springer},
 address      = {Trento},
 pages        = {202--206},
 doi          = {10.1007/3-540-48660-7\_14},
)
@inproceedings(schurmann03tphols,
 author       = {Carsten Sch{\"u}rmann and Frank Pfenning},
 year         = {2003},
 title        = {A Coverage Checking Algorithm for {LF}},
 booktitle    = {Theorem Proving in Higher Order Logics: 16th International Conference, TPHOLs 2003},
 series       = {LNCS},
 volume       = {2758},
 publisher    = {Springer},
 pages        = {120--135},
 doi          = {10.1007/10930755\_8},
)
@inproceedings(wilson10coq,
 author       = {Sean Wilson and Jacques Fleuriot and Alan Smaill},
 year         = {2010},
 title        = {Inductive Proof Automation for {Coq}},
 booktitle    = {Second Coq Workshop},
 url          = {http://hal.archives-ouvertes.fr/inria-00489496/en/},
)