@article(andreoli92jlc,
 author       = {Jean-Marc Andreoli},
 year         = {1992},
 title        = {Logic Programming with Focusing Proofs in Linear Logic},
 journal      = {J. of Logic and Computation},
 volume       = {2},
 number       = {3},
 pages        = {297--347},
 doi          = {10.1093/logcom/2.3.297},
)
@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},
)
@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},
)
@inproceedings(baelde07cade,
 author       = {David Baelde and Andrew Gacek and Dale Miller and Gopalan Nadathur and Alwen Tiu},
 year         = {2007},
 title        = {The {Bedwyr} system for model checking over syntactic expressions},
 editor       = {F. Pfenning},
 booktitle    = {21th Conf.\ on Automated Deduction (CADE)},
 series       = {LNAI},
 volume       = {4603},
 publisher    = {Springer},
 address      = {New York},
 pages        = {391--397},
 doi          = {10.1007/978-3-540-73595-3\_28},
)
@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(clarke99book,
 author       = {Edmund M. Clarke and Orna Grumberg and Doron A. Peled},
 year         = {1999},
 title        = {Model Checking},
 publisher    = {The {MIT} Press},
 address      = {Cambridge, Massachusetts},
)
@article(delande10apal,
 author       = {Olivier Delande and Dale Miller and Alexis Saurin},
 year         = {2010},
 title        = {Proof and refutation in {MALL} as a game},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {161},
 number       = {5},
 pages        = {654--672},
 doi          = {10.1016/j.apal.2009.07.017},
)
@article(gacek11ic,
 author       = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
 year         = {2011},
 title        = {Nominal abstraction},
 journal      = {Information and Computation},
 volume       = {209},
 number       = {1},
 pages        = {48--73},
 doi          = {10.1016/j.ic.2010.09.004},
)
@article(girard87tcs,
 author       = {Jean-Yves Girard},
 year         = {1987},
 title        = {Linear Logic},
 journal      = {Theoretical Computer Science},
 volume       = {50},
 pages        = {1--102},
 doi          = {10.1016/0304-3975(87)90045-4},
)
@unpublished(girard92mail,
 author       = {Jean-Yves Girard},
 year         = {1992},
 title        = {A Fixpoint Theorem in Linear Logic},
 note         = {An email posting to the mailing list linear@cs.stanford.edu},
)
@article(hennessy85jacma,
 author       = {Matthew Hennessy and Robin Milner},
 year         = {1985},
 title        = {Algebraic Laws for Nondeterminism and Concurrency},
 journal      = {JACM},
 volume       = {32},
 number       = {1},
 pages        = {137--161},
 doi          = {10.1145/2455.2460},
)
@article(mcdowell00tcs,
 author       = {Raymond McDowell and Dale Miller},
 year         = {2000},
 title        = {Cut-elimination for a logic with definitions and induction},
 journal      = {Theoretical Computer Science},
 volume       = {232},
 pages        = {91--119},
 doi          = {10.1016/S0304-3975(99)00171-1},
)
@inproceedings(miller11cpp,
 author       = {Dale Miller},
 year         = {2011},
 title        = {A proposal for broad spectrum proof certificates},
 editor       = {J.-P. Jouannaud and Z. Shao},
 booktitle    = {CPP: First International Conference on Certified Programs and Proofs},
 series       = {LNCS},
 volume       = {7086},
 pages        = {54--69},
 doi          = {10.1007/978-3-642-25379-9\_6},
)
@book(miller12proghol,
 author       = {Dale Miller and Gopalan Nadathur},
 year         = {2012},
 title        = {Programming with Higher-Order Logic},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139021326},
)
@article(miller91apal,
 author       = {Dale Miller and Gopalan Nadathur and Frank Pfenning and Andre Scedrov},
 year         = {1991},
 title        = {Uniform Proofs as a Foundation for Logic Programming},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {51},
 pages        = {125--157},
 doi          = {10.1016/0168-0072(91)90068-W},
)
@article(miller05tocl,
 author       = {Dale Miller and Alwen Tiu},
 year         = {2005},
 title        = {A proof theory for generic judgments},
 journal      = {ACM Trans.\ on Computational Logic},
 volume       = {6},
 number       = {4},
 pages        = {749--783},
 doi          = {10.1145/1094622.1094628},
)
@book(milner89book,
 author       = {Robin Milner},
 year         = {1989},
 title        = {Communication and Concurrency},
 publisher    = {Prentice-Hall International},
)
@incollection(pous11atbc,
 author       = {Damien Pous and Davide Sangiorgi},
 year         = {2011},
 title        = {Enhancements of the bisimulation proof method},
 editor       = {Davide Sangiorgi and Jan Rutten},
 booktitle    = {Advanced Topics in Bisimulation and Coinduction},
 publisher    = {Cambridge University Press},
 pages        = {233--289},
 doi          = {10.1017/CBO9780511792588.007},
)
@inproceedings(schroeder-heister93lics,
 author       = {Schroeder-Heister, Peter},
 year         = {1993},
 title        = {Rules of Definitional Reflection},
 editor       = {M. Vardi},
 booktitle    = {8th Symp.\ on Logic in Computer Science},
 organization = {IEEE Computer Society Press},
 publisher    = {IEEE},
 pages        = {222--232},
 doi          = {10.1109/LICS.1993.287585},
)
@inproceedings(tiu05eshol,
 author       = {Alwen Tiu and Gopalan Nadathur and Dale Miller},
 year         = {2005},
 title        = {Mixing Finite Success and Finite Failure in an Automated Prover},
 booktitle    = {Empirically Successful Automated Reasoning in Higher-Order Logics (ESHOL'05)},
 pages        = {79--98},
)
@misc(Bedwyr,
 year         = {2015},
 title        = {The {B}edwyr model checker},
 note         = {Available at \url{http://slimmer.gforge.inria.fr/bedwyr/}},
)