References

  1. Jonathan Aldrich, Robert J. Simmons & Key Shin (2008): SASyLF: An Educational Proof Assistant for Language Theory. In: International Workshop on Functional and Declarative Programming in Education. ACM Press, pp. 31–40, doi:10.1145/1411260.1411266.
  2. 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: Eighteenth International Conference on Theorem Proving in Higher Order Logics, LNCS 3603. Springer, pp. 50–65, doi:10.1007/11541868_4.
  3. Christoph Benzmüller, Florian Rabe & Geoff Sutcliffe (2008): THF0—The Core of the TPTP Language for Higher-Order Logic. In: Fourth International Joint Conference on Automated Reasoning, LNCS 5195. Springer, pp. 491–506, doi:10.1007/978-3-540-71070-7_41.
  4. Andrew Cave & Brigitte Pientka (2012): Programming with Binders and Indexed Data-Types. In: Thirty-Ninth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, pp. 413–424, doi:10.1145/2103656.2103705.
  5. Matthias Felleisen, Robert Bruce Findler & Matthew Flatt (2009): Semantics Engineering with PLT Redex. The MIT Press.
  6. Amy P. Felty & Alberto 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.
  7. Amy P. Felty, Alberto Momigliano & Brigitte Pientka (2015): The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1—A Common Infrastructure for Benchmarks. CoRR abs/1503.06095. Available at http://arxiv.org/abs/1503.06095.
  8. Amy P. Felty, Alberto Momigliano & Brigitte Pientka (2015): The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 2—A Survey. Journal of Automated Reasoning. (to appear).
  9. Jean-Christophe Filliâtre (2013): One Logic To Use Them All. In: Twenty-Fourth International Conference on Automated Deduction, LNCS 7898. Springer, pp. 1–20, doi:10.1007/978-3-642-38574-2_1.
  10. Andrew Gacek (2008): The Abella Interactive Theorem Prover (System Description). In: Fourth International Joint Conference on Automated Reasoning, LNCS 5195. Springer, pp. 154–161, doi:10.1007/978-3-540-71070-7_13.
  11. Andrew Gacek, Dale Miller & Gopalan Nadathur (2012): A Two-Level Logic Approach to Reasoning About Computations. Journal of Automated Reasoning 49(2), pp. 241–273, doi:10.1007/s10817-011-9218-1.
  12. J.-Y. Girard, Y. Lafont & P. Tayor (1990): Proofs and Types. Cambridge University Press.
  13. Nada Habli & Amy P. Felty (2013): Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs. In: Third International Workshop on Proof Exchange for Theorem Proving, EasyChair Proceedings in Computing 14, pp. 67–76.
  14. Holger H. Hoos & Thomas Stützle (2000): SATLIB: An Online Resource for Research on SAT. In: SAT 2000: Highlights of Satisfiability Research in the Year 2000, Frontiers in Artificial Intelligence and Applications 63. IOS Press, pp. 283–292.
  15. Alberto Momigliano, Alan J. Martin & Amy P. Felty (2008): Two-Level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax. In: Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2007, ENTCS 196. Elsevier, pp. 85–93, doi:10.1016/j.entcs.2007.09.019.
  16. Brigitte Pientka (2007): Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF. In: Twentieth International Conference on Theorem Proving in Higher-Order Logics, LNCS. Springer, pp. 246–261, doi:10.1007/978-3-540-74591-4_19.
  17. Brigitte Pientka & Andrew Cave (2015): Inductive Beluga:Programming Proofs (System Description). In: Twenty-Fifth International Conference on Automated Deduction. Springer.
  18. Brigitte Pientka & Joshua Dunfield (2010): Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). In: Fifth International Joint Conference on Automated Reasoning, LNCS 6173. Springer, pp. 15–21, doi:10.1007/978-3-642-14203-1_2.
  19. Benjamin C. Pierce (2002): Types and Programming Languages. MIT Press.
  20. Adam Poswolsky & Carsten Schürmann (2009): System Description: Delphin—A Functional Programming Language for Deductive Systems. In: Third International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), ENTCS 228. Elsevier, pp. 113–120, doi:10.1016/j.entcs.2008.12.120.
  21. Florian Rabe & Carsten Schürmann (2009): A Practical Module System for LF. In: Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice. ACM Press, pp. 40–48, doi:10.1145/1577824.1577831.
  22. Grigore Roşu & Traian Florin Şerbănuţă (2010): An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming 79(6), pp. 397–434, doi:10.1016/j.jlap.2010.03.012.
  23. Carsten Schürmann (2009): The Twelf Proof Assistant. In: Twenty-Second International Conference on Theorem Proving in Higher Order Logics, LNCS 5674. Springer, pp. 79–83, doi:10.1007/978-3-642-03359-9_7.
  24. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar & Rok Strniša (2010): Ott: Effective Tool Support for the Working Semanticist. Journal of Functional Programming 20(1), pp. 71–122, doi:10.1017/S0956796809990293.
  25. Geoff Sutcliffe (2009): The TPTP Problem Library and Associated Infrastructure. Journal of Automated Reasoning 43(4), pp. 337–362, doi:10.1007/s10817-009-9143-8.
  26. Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek & Gopalan Nadathur (2013): Reasoning About Higher-Order Relational Specifications. In: Fifteenth International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming. ACM Press, pp. 157–168, doi:10.1145/2505879.2505889.

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