References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. G. Gonthier & A. Mahboubi (2008): A Small Scale Reflection Extension for the Coq system. Technical Report RR-6455. INRIA.
  11. 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.
  12. 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.
  13. M. Iancu (2017): Towards Flexiformal Mathematics. Jacobs University Bremen.
  14. 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.
  15. Dennis Müller, Florian Rabe & Michael Kohlhase (2018): Theories as Types. In: Didier Galmiche, Stephan Schulz & Roberto Sebastiani: Automated Reasoning. Springer Verlag, doi:10.1007/978-3-319-94205-6_38. Available at http://kwarc.info/kohlhase/papers/ijcar18-records.pdf.
  16. L. Paulson (1994): Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science 828. Springer, doi:10.1007/BFb0030556.
  17. 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.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. Florian Rabe (2018): A Modular Type Reconstruction Algorithm. ACM Trans. Comput. Logic 19(4), pp. 24:1–24:43, doi:10.1145/3234693.
  23. 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.
  24. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org