A. Asperti, W. Ricciotti, C. Sacerdoti Coen & E. Tassi (2009):
Hints in Unification.
In: S. Berghofer, T. Nipkow, C. Urban & M. Wenzel: Theorem Proving in Higher Order Logics.
Springer,
pp. 84–98,
doi:10.1007/BFb0028402.
M. Boespflug, Q. Carbonneaux & O. Hermant (2012):
The λΠ-calculus modulo as a universal proof language.
In: D. Pichardie & T. Weber: Proceedings of PxTP2012: Proof Exchange for Theorem Proving,
pp. 28–43,
doi:10.1007/978-3-642-38574-2_11.
J. Carette & R. O'Connor (2012):
Theory Presentation Combinators.
In: J. Jeuring, J. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel & V. Sorge: Intelligent Computer Mathematics 7362.
Springer,
pp. 202–215,
doi:10.1017/S0960129511000119.
D. Christiansen & E. Brady (2016):
Elaborator reflection: extending Idris in Idris.
In: J. Garrigue, G. Keller & E. Sumii: International Conference on Functional Programming.
ACM,
pp. 284–297,
doi:10.1145/3022670.2951932.
D. Cousineau & G. Dowek (2007):
Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo.
In: S. Ronchi Della Rocca: Typed Lambda Calculi and Applications.
Springer,
pp. 102–117,
doi:10.1145/138027.138060.
C. Dunchev, F. Guidi, C. Sacerdoti Coen & E. Tassi (2015):
ELPI: Fast, Embeddable, lambda-Prolog Interpreter.
In: M. Davis, A. Fehnker, A. McIver & A. Voronkov: Logic for Programming, Artificial Intelligence, and Reasoning,
pp. 460–468,
doi:10.1007/978-3-540-71067-7_23.
G. Ebner, S. Ullrich, J. Roesch, J. Avigad & L. de Moura (2017):
A Metaprogramming Framework for Formal Verification.
Proceedings of the ACM on Programming Languages 1(ICFP),
pp. 34:1–34:29,
doi:10.1145/3110278.
A. Felty & A. Momigliano (2012):
Hybrid - A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax.
Journal of Automated Reasoning 48(1),
pp. 43–105,
doi:10.1007/s10817-010-9194-x.
A. Gacek (2008):
The Abella Interactive Theorem Prover (System Description).
In: A. Armando, P. Baumgartner & G. Dowek: Automated Reasoning,
pp. 154–161,
doi:10.2307/2271658.
G. Gonthier & A. Mahboubi (2008):
A Small Scale Reflection Extension for the Coq system.
Technical Report RR-6455.
INRIA.
R. Harper, F. Honsell & G. Plotkin (1993):
A framework for defining logics.
Journal of the Association for Computing Machinery 40(1),
pp. 143–184,
doi:10.1145/138027.138060.
F. Honsell, L. Liquori, P. Maksimovic & I. Scagnetto (2017):
LLFP: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads.
Logical Methods in Computer Science 13(3),
doi:10.23638/LMCS-13(3:2)2017.
M. Iancu (2017):
Towards Flexiformal Mathematics.
Jacobs University Bremen.
M. Kohlhase, D. Müller, S. Owre & F. Rabe (2017):
Making PVS Accessible to Generic Services by Interpretation in a Universal Format.
In: M. Ayala-Rincon & C. Munoz: Interactive Theorem Proving.
Springer,
pp. 319–335,
doi:10.1007/978-3-319-08434-3.
L. Paulson (1994):
Isabelle: A Generic Theorem Prover.
Lecture Notes in Computer Science 828.
Springer,
doi:10.1007/BFb0030556.
F. Pfenning & C. Schürmann (1999):
System Description: Twelf - A Meta-Logical Framework for Deductive Systems.
In: H. Ganzinger: Automated Deduction,
pp. 202–206,
doi:10.1007/3-540-48660-7_14.
B. Pientka & J. Dunfield (2010):
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System description).
In: J. Giesl & R. Hähnle: Automated Reasoning.
Springer,
pp. 15–21,
doi:10.1145/1389449.1389469.
F. Rabe (2013):
The MMT API: A Generic MKM System.
In: J. Carette, D. Aspinall, C. Lange, P. Sojka & W. Windsteiger: Intelligent Computer Mathematics.
Springer,
pp. 339–343,
doi:10.1007/978-3-642-31374-5_10.
F. Rabe (2017):
How to Identify, Translate, and Combine Logics?.
Journal of Logic and Computation 27(6),
pp. 1753–1798,
doi:10.1093/logcom/exu079.
F. Rabe & M. Kohlhase (2013):
A Scalable Module System.
Information and Computation 230(1),
pp. 1–54,
doi:10.1016/j.ic.2013.06.001.
Florian Rabe (2018):
A Modular Type Reconstruction Algorithm.
ACM Trans. Comput. Logic 19(4),
pp. 24:1–24:43,
doi:10.1145/3234693.
The Univalent Foundations Program (2013):
Homotopy Type Theory: Univalent Foundations of Mathematics.
http://homotopytypetheory.org/book,
Institute for Advanced Study,
doi:10.1007/978-3-642-20920-8_4.
K. Watkins, I. Cervesato, F. Pfenning & D. Walker (2002):
A Concurrent Logical Framework I: Judgments and Properties.
Technical Report CMU-CS-02-101.
Department of Computer Science, Carnegie Mellon University,
doi:10.21236/ADA418517.