@inproceedings(matitahints,
 author       = {A. Asperti and W. Ricciotti and C. Sacerdoti Coen and E. Tassi},
 year         = {2009},
 title        = {Hints in Unification},
 editor       = {S. Berghofer and T. Nipkow and C. Urban and M. Wenzel},
 booktitle    = {Theorem Proving in Higher Order Logics},
 publisher    = {Springer},
 pages        = {84--98},
 doi          = {10.1007/BFb0028402},
)
@inproceedings(dedukti,
 author       = {M. Boespflug and Q. Carbonneaux and O. Hermant},
 year         = {2012},
 title        = {The {$\lambda\Pi $}-calculus modulo as a universal proof language},
 editor       = {D. Pichardie and T. Weber},
 booktitle    = {Proceedings of PxTP2012: Proof Exchange for Theorem Proving},
 pages        = {28--43},
 doi          = {10.1007/978-3-642-38574-2_11},
)
@inproceedings(mathschemetheoexp,
 author       = {J. Carette and R. O'Connor},
 year         = {2012},
 title        = {{Theory Presentation Combinators}},
 editor       = {J. Jeuring and J. Campbell and J. Carette and G. Dos Reis and P. Sojka and M. Wenzel and V. Sorge},
 booktitle    = {Intelligent Computer Mathematics},
 volume       = {7362},
 publisher    = {Springer},
 pages        = {202--215},
 doi          = {10.1017/S0960129511000119},
)
@inproceedings(idrisreflection,
 author       = {D. Christiansen and E. Brady},
 year         = {2016},
 title        = {Elaborator reflection: extending {Idris} in {Idris}},
 editor       = {J. Garrigue and G. Keller and E. Sumii},
 booktitle    = {International Conference on Functional Programming},
 publisher    = {ACM},
 pages        = {284--297},
 doi          = {10.1145/3022670.2951932},
)
@inproceedings(lambdaPimodulo,
 author       = {D. Cousineau and G. Dowek},
 year         = {2007},
 title        = {Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo},
 editor       = {S. Ronchi Della Rocca},
 booktitle    = {Typed Lambda Calculi and Applications},
 publisher    = {Springer},
 pages        = {102--117},
 doi          = {10.1145/138027.138060},
)
@inproceedings(elpi,
 author       = {C. Dunchev and F. Guidi and C. Sacerdoti Coen and E. Tassi},
 year         = {2015},
 title        = {{ELPI: Fast, Embeddable, lambda-Prolog Interpreter}},
 editor       = {M. Davis and A. Fehnker and A. McIver and A. Voronkov},
 booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning},
 pages        = {460--468},
 doi          = {10.1007/978-3-540-71067-7_23},
)
@article(leanreflection,
 author       = {G. Ebner and S. Ullrich and J. Roesch and J. Avigad and {de Moura}, L.},
 year         = {2017},
 title        = {{A Metaprogramming Framework for Formal Verification}},
 journal      = {Proceedings of the {ACM} on Programming Languages},
 volume       = {1},
 number       = {ICFP},
 pages        = {34:1--34:29},
 doi          = {10.1145/3110278},
)
@article(hybrid,
 author       = {A. Felty and A. Momigliano},
 year         = {2012},
 title        = {Hybrid - A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax},
 journal      = {Journal of Automated Reasoning},
 volume       = {48},
 number       = {1},
 pages        = {43--105},
 doi          = {10.1007/s10817-010-9194-x},
)
@inproceedings(abella,
 author       = {A. Gacek},
 year         = {2008},
 title        = {The {A}bella Interactive Theorem Prover (System Description)},
 editor       = {A. Armando and P. Baumgartner and G. Dowek},
 booktitle    = {Automated Reasoning},
 pages        = {154--161},
 doi          = {10.2307/2271658},
)
@techreport(coqssreflect,
 author       = {G. Gonthier and A. Mahboubi},
 year         = {2008},
 title        = {{A Small Scale Reflection Extension for the Coq system}},
 type         = {Technical Report},
 number       = {{RR-6455}},
 institution  = {{INRIA}},
)
@article(lf,
 author       = {R. Harper and F. Honsell and G. Plotkin},
 year         = {1993},
 title        = {{A framework for defining logics}},
 journal      = {{Journal of the Association for Computing Machinery}},
 volume       = {40},
 number       = {1},
 pages        = {143--184},
 doi          = {10.1145/138027.138060},
)
@article(llfp,
 author       = {F. Honsell and L. Liquori and P. Maksimovic and I. Scagnetto},
 year         = {2017},
 title        = {{LLFP}: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads},
 journal      = {Logical Methods in Computer Science},
 volume       = {13},
 number       = {3},
 doi          = {10.23638/LMCS-13(3:2)2017},
)
@phdthesis(Iancu:phd,
 author       = {M. Iancu},
 year         = {2017},
 title        = {{Towards Flexiformal Mathematics}},
 school       = {Jacobs University Bremen},
)
@inproceedings(KMOR:pvs:17,
 author       = {M. Kohlhase and D. M{\"u}ller and S. Owre and F. Rabe},
 year         = {2017},
 title        = {{Making PVS Accessible to Generic Services by Interpretation in a Universal Format}},
 editor       = {Ayala-Rincon, M. and C. Munoz},
 booktitle    = {Interactive Theorem Proving},
 publisher    = {Springer},
 pages        = {319--335},
 doi          = {10.1007/978-3-319-08434-3},
)
@inproceedings(MueRabKoh:tat18,
 author       = {Dennis M{\"u}ller and Florian Rabe and Michael Kohlhase},
 year         = {2018},
 title        = {Theories as Types},
 editor       = {Didier Galmiche and Stephan Schulz and Roberto Sebastiani},
 booktitle    = {Automated Reasoning},
 publisher    = {Springer Verlag},
 doi          = {10.1007/978-3-319-94205-6_38},
 url          = {http://kwarc.info/kohlhase/papers/ijcar18-records.pdf},
)
@book(isabelle,
 author       = {L. Paulson},
 year         = {1994},
 title        = {{Isabelle: A Generic Theorem Prover}},
 series       = {Lecture Notes in Computer Science},
 volume       = {828},
 publisher    = {Springer},
 doi          = {10.1007/BFb0030556},
)
@inproceedings(twelf,
 author       = {F. Pfenning and C. Sch{\"u}rmann},
 year         = {1999},
 title        = {System Description: {Twelf} - A Meta-Logical Framework for Deductive Systems},
 editor       = {H. Ganzinger},
 booktitle    = {Automated Deduction},
 pages        = {202--206},
 doi          = {10.1007/3-540-48660-7_14},
)
@inproceedings(beluga,
 author       = {B. Pientka and J. 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    = {{Automated Reasoning}},
 publisher    = {Springer},
 pages        = {15--21},
 doi          = {10.1145/1389449.1389469},
)
@inproceedings(rabe:mmtabs:13,
 author       = {F. Rabe},
 year         = {2013},
 title        = {{The MMT API: A Generic MKM System}},
 editor       = {J. Carette and D. Aspinall and C. Lange and P. Sojka and W. Windsteiger},
 booktitle    = {Intelligent Computer Mathematics},
 publisher    = {Springer},
 pages        = {339--343},
 doi          = {10.1007/978-3-642-31374-5_10},
)
@article(rabe:howto:14,
 author       = {F. Rabe},
 year         = {2017},
 title        = {{How to Identify, Translate, and Combine Logics?}},
 journal      = {Journal of Logic and Computation},
 volume       = {27},
 number       = {6},
 pages        = {1753--1798},
 doi          = {10.1093/logcom/exu079},
)
@article(RK:mmt:10,
 author       = {F. Rabe and M. Kohlhase},
 year         = {2013},
 title        = {{A Scalable Module System}},
 journal      = {Information and Computation},
 volume       = {230},
 number       = {1},
 pages        = {1--54},
 doi          = {10.1016/j.ic.2013.06.001},
)
@article(rabe:recon:17,
 author       = {Florian Rabe},
 year         = {2018},
 title        = {A Modular Type Reconstruction Algorithm},
 journal      = {ACM Trans. Comput. Logic},
 volume       = {19},
 number       = {4},
 pages        = {24:1--24:43},
 doi          = {10.1145/3234693},
)
@book(hottbook,
 author       = {{Univalent Foundations Program}, The},
 year         = {2013},
 title        = {Homotopy Type Theory: Univalent Foundations of Mathematics},
 publisher    = {\url{http://homotopytypetheory.org/book}},
 address      = {Institute for Advanced Study},
 doi          = {10.1007/978-3-642-20920-8_4},
)
@techreport(clf,
 author       = {K. Watkins and I. Cervesato and F. Pfenning and D. Walker},
 year         = {2002},
 title        = {{A Concurrent Logical Framework I: Judgments and Properties}},
 type         = {Technical Report},
 number       = {CMU-CS-02-101},
 institution  = {{Department of Computer Science, Carnegie Mellon University}},
 doi          = {10.21236/ADA418517},
)