References

  1. The Adelfa System. http://adelfa.cs.umn.edu/.
  2. The Twelf Project. http://twelf.org/.
  3. Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich & Steve Zdancewic (2005): Mechanized Metatheory for the Masses: The POPLmark Challenge. In: Theorem Proving in Higher Order Logics: 18th International Conference, LNCS 3603. Springer, pp. 50–65, doi:10.1007/11541868_4.
  4. David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu & Yuting Wang (2014): Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning 7(2), doi:10.6092/issn.1972-5787/4650. Available at http://jfr.unibo.it/article/download/4650/4137.
  5. Amy Felty & Dale Miller (1990): Encoding a Dependent-Type λ-Calculus in a Logic Programming Language. In: Mark Stickel: Proceedings of the 1990 Conference on Automated Deduction, LNAI 449. Springer, pp. 221–235, doi:10.1007/3-540-52885-7_90.
  6. Andrew Gacek (2009): A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. University of Minnesota.
  7. Andrew Gacek, Dale Miller & Gopalan Nadathur (2011): Nominal Abstraction. Information and Computation 209(1), pp. 48–73, doi:10.1016/j.ic.2010.09.004.
  8. Robert Harper, Furio Honsell & Gordon Plotkin (1993): A Framework for Defining Logics. Journal of the ACM 40(1), pp. 143–184, doi:10.1145/138027.138060.
  9. Robert Harper & Daniel R. Licata (2007): Mechanizing Metatheory in a Logical Framework. Journal of Functional Programming 17(4–5), pp. 613–673, doi:10.1017/S0956796807006430.
  10. Dale Miller (1991): A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification. J. of Logic and Computation 1(4), pp. 497–536, doi:10.1093/logcom/1.4.497.
  11. Dale Miller (1992): Unification Under a Mixed Prefix. Journal of Symbolic Computation 14(4), pp. 321–358, doi:10.1016/0747-7171(92)90011-R.
  12. Gopalan Nadathur & Natalie Linnell (2005): Practical Higher-Order Pattern Unification With On-the-Fly Raising. In: ICLP 2005: 21st International Logic Programming Conference, LNCS 3668. Springer, Sitges, Spain, pp. 371–386, doi:10.1007/11562931_28.
  13. Gopalan Nadathur & Mary Southern (2021): A Logic for Reasoning About LF Specifications. Available from http://arxiv.org/abs/2107.00111..
  14. Aleksandar Nanevski, Frank Pfenning & Brigitte Pientka (2008): Contextual Model Type Theory. ACM Trans. on Computational Logic 9(3), pp. 1–49, doi:10.1145/1352582.1352591.
  15. Frank Pfenning & Carsten Schürmann (1999): System Description: Twelf — A Meta-Logical Framework for Deductive Systems. In: H. Ganzinger: 16th Conf. on Automated Deduction (CADE), LNAI 1632. Springer, Trento, pp. 202–206, doi:10.1007/3-540-48660-7_14.
  16. Frank Pfenning & Carsten Schürmann (2002): Twelf User's Guide. Available from http://www.cs.cmu.edu/~twelf/guide-1-4.
  17. Brigitte Pientka & Joshua Dunfield (2010): Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). In: J. Giesl & R. Hähnle: Fifth International Joint Conference on Automated Reasoning, LNCS 6173, pp. 15–21, doi:10.1007/978-3-642-14203-1_2.
  18. Carsten Schürmann (2000): Automating the Meta Theory of Deductive Systems. Carnegie Mellon University. Available at http://www.cs.yale.edu/homes/carsten/papers/S00b.ps.gz.
  19. Mary Southern (2021): A Framework for Reasoning About LF Specifications. University of Minnesota.
  20. Mary Southern & Kaustuv Chaudhuri (2014): A Two-Level Logic Approach to Reasoning About Typed Specification Languages. In: Venkatesh Raman & S. P. Suresh: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014), Leibniz International Proceedings in Informatics (LIPIcs) 29, Dagstuhl, Germany, pp. 557–569, doi:10.4230/LIPIcs.FSTTCS.2014.557. Available at http://drops.dagstuhl.de/opus/volltexte/2014/4871.
  21. Alwen Tiu (2006): A Logic for Reasoning about Generic Judgments. In: A. Momigliano & B. Pientka: Int. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06), ENTCS 173, pp. 3–18, doi:10.1016/j.entcs.2007.01.016.
  22. Yuting Wang & Gopalan Nadathur (2013): Towards Extracting Explicit Proofs from Totality Checking in Twelf. In: LFMTP 2013 - Proceedings of the 2013 ACM SIGPLAN Workshop on Logical Frameworks and Meta-Languages, pp. 55–66, doi:10.1145/2503887.2503893.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org