@misc(adelfa.website,
 title        = {The {A}delfa System},
 howpublished = {\url{http://adelfa.cs.umn.edu/}},
)
@misc(twelf.website,
 title        = {The {T}welf Project},
 howpublished = {\url{http://twelf.org/}},
)
@inproceedings(aydemir05tphols,
 author       = {Brian E. Aydemir and Aaron Bohannon and Matthew Fairbairn and J. Nathan Foster and Benjamin C. Pierce and Peter Sewell and Dimitrios Vytiniotis and Geoffrey Washburn and Stephanie Weirich and Steve Zdancewic},
 year         = {2005},
 title        = {Mechanized Metatheory for the Masses: The {POPLmark} Challenge},
 booktitle    = {Theorem Proving in Higher Order Logics: 18th International Conference},
 series       = {LNCS},
 volume       = {3603},
 publisher    = {Springer},
 pages        = {50--65},
 doi          = {10.1007/11541868_4},
)
@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(felty90cade,
 author       = {Amy Felty and Dale Miller},
 year         = {1990},
 title        = {Encoding a Dependent-Type $\lambda$-Calculus in a Logic Programming Language},
 editor       = {Mark Stickel},
 booktitle    = {Proceedings of the 1990 Conference on Automated Deduction},
 series       = {LNAI},
 volume       = {449},
 publisher    = {Springer},
 pages        = {221--235},
 doi          = {10.1007/3-540-52885-7_90},
)
@phdthesis(gacek09phd,
 author       = {Andrew Gacek},
 year         = {2009},
 title        = {A Framework for Specifying, Prototyping, and Reasoning about Computational Systems},
 school       = {University of Minnesota},
)
@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(harper93jacm,
 author       = {Robert Harper and Furio Honsell and Gordon Plotkin},
 year         = {1993},
 title        = {A Framework for Defining Logics},
 journal      = {Journal of the ACM},
 volume       = {40},
 number       = {1},
 pages        = {143--184},
 doi          = {10.1145/138027.138060},
)
@article(harper07jfp,
 author       = {Robert Harper and Daniel R. Licata},
 year         = {2007},
 title        = {Mechanizing Metatheory in a Logical Framework},
 journal      = {Journal of Functional Programming},
 volume       = {17},
 number       = {4--5},
 pages        = {613--673},
 doi          = {10.1017/S0956796807006430},
)
@article(miller91jlc,
 author       = {Dale Miller},
 year         = {1991},
 title        = {A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification},
 journal      = {J. of Logic and Computation},
 volume       = {1},
 number       = {4},
 pages        = {497--536},
 doi          = {10.1093/logcom/1.4.497},
)
@article(miller92jsc,
 author       = {Dale Miller},
 year         = {1992},
 title        = {Unification Under a Mixed Prefix},
 journal      = {Journal of Symbolic Computation},
 volume       = {14},
 number       = {4},
 pages        = {321--358},
 doi          = {10.1016/0747-7171(92)90011-R},
)
@inproceedings(nadathur05iclp,
 author       = {Gopalan Nadathur and Natalie Linnell},
 year         = {2005},
 title        = {Practical Higher-Order Pattern Unification With On-the-Fly Raising},
 booktitle    = {{ICLP 2005: 21st International Logic Programming Conference}},
 series       = {LNCS},
 volume       = {3668},
 publisher    = {Springer},
 address      = {Sitges, Spain},
 pages        = {371--386},
 doi          = {10.1007/11562931_28},
)
@unpublished(nadathur21arxiv,
 author       = {Gopalan Nadathur and Mary Southern},
 year         = {2021},
 title        = {A Logic for Reasoning About {LF} Specifications},
 note         = {Available from \url{http://arxiv.org/abs/2107.00111}.},
)
@article(nanevski08tocl,
 author       = {Aleksandar Nanevski and Frank Pfenning and Brigitte Pientka},
 year         = {2008},
 title        = {Contextual Model Type Theory},
 journal      = {ACM Trans.\ on Computational Logic},
 volume       = {9},
 number       = {3},
 pages        = {1--49},
 doi          = {10.1145/1352582.1352591},
)
@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},
)
@manual(Pfenning02guide,
 author       = {Frank Pfenning and Carsten Sch{\"u}rmann},
 year         = {2002},
 title        = {Twelf User's Guide},
 note         = {Available from \url{http://www.cs.cmu.edu/~twelf/guide-1-4}},
)
@inproceedings(pientka10ijcar,
 author       = {Brigitte Pientka and Joshua Dunfield},
 year         = {2010},
 title        = {Beluga: {A} Framework for Programming and Reasoning with Deductive Systems (System Description)},
 editor       = {J. Giesl and R. H{\"a}hnle},
 booktitle    = {Fifth International Joint Conference on Automated Reasoning},
 series       = {LNCS},
 volume       = {6173},
 pages        = {15--21},
 doi          = {10.1007/978-3-642-14203-1_2},
)
@phdthesis(schurmann00phd,
 author       = {Carsten Sch{\"{u}}rmann},
 year         = {2000},
 title        = {Automating the Meta Theory of Deductive Systems},
 school       = {Carnegie Mellon University},
 url          = {http://www.cs.yale.edu/homes/carsten/papers/S00b.ps.gz},
)
@phdthesis(southern21phd,
 author       = {Mary Southern},
 year         = {2021},
 title        = {A Framework for Reasoning About LF Specifications},
 school       = {University of Minnesota},
)
@inproceedings(southern14fsttcs,
 author       = {Mary Southern and Kaustuv Chaudhuri},
 year         = {2014},
 title        = {A Two-Level Logic Approach to Reasoning About Typed Specification Languages},
 editor       = {Venkatesh Raman and S. P. Suresh},
 booktitle    = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
 series       = {Leibniz International Proceedings in Informatics (LIPIcs)},
 volume       = {29},
 address      = {Dagstuhl, Germany},
 pages        = {557--569},
 doi          = {10.4230/LIPIcs.FSTTCS.2014.557},
 url          = {http://drops.dagstuhl.de/opus/volltexte/2014/4871},
)
@inproceedings(tiu06lfmtp,
 author       = {Alwen Tiu},
 year         = {2006},
 title        = {A Logic for Reasoning about Generic Judgments},
 editor       = {A. Momigliano and B. Pientka},
 booktitle    = {Int. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06)},
 series       = {ENTCS},
 volume       = {173},
 pages        = {3--18},
 doi          = {10.1016/j.entcs.2007.01.016},
)
@inproceedings(wang13lfmtp,
 author       = {Yuting Wang and Gopalan Nadathur},
 year         = {2013},
 title        = {Towards Extracting Explicit Proofs from Totality Checking in {T}welf},
 booktitle    = {LFMTP 2013 - Proceedings of the 2013 ACM SIGPLAN Workshop on Logical Frameworks and Meta-Languages},
 pages        = {55--66},
 doi          = {10.1145/2503887.2503893},
)