
Hybrid is implemented as the following files, which are used in all of the examples that follow, and must be compiled in the order they appear.





[FMP17] Benchmarks for Reasoning with Syntax Trees Containing Binders and Contexts of Assumptions, by Amy Felty, Alberto Momigliano, and Brigitte Pientka. In Mathematical Structures in Computer Science, Cambridge University Press, pages 134, May 2017 (pdf). [BF16] The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid, by Chelsea Battell and Amy Felty. In Proceedings of the Eleventh International Workshop on Logical Frameworks and MetaLanguages: Theory and Practice (LFMTP), June 2016 (pdf). [FMP15a] The Next 700 Challenge Problems for Reasoning with HigherOrder Abstract Syntax Representations: Part 1–A Common Infrastructure for Benchmarks, by Amy P. Felty, Alberto Momigliano, and Brigitte Pientka, 2015, (arXiv, pdf). [FMP15b] The Next 700 Challenge Problems for Reasoning with HigherOrder Abstract Syntax Representations: Part 2–A Survey, by Amy P. Felty, Alberto Momigliano, and Brigitte Pientka, Journal of Automated Reasoning, 2015, to appear (pdf). [FMP15c] An Open Challenge Problem Repository for Systems Supporting Binders, by Amy Felty, Alberto Momigliano, and Brigitte Pientka, In Proceedings of the Tenth International Workshop on Logical Frameworks and MetaLanguages: Theory and Practice (LFMTP), in Electronic Proceedings in Theoretical Computer Science, Volume 185, pages 1832, August 2015 (pdf). [HF13] Translating HigherOrder Specifications to Coq Libraries Supporting Hybrid Proofs, by Nada Habli and Amy Felty. In Third International Workshop on Proof Exchange for Theorem Proving, EasyChair Proceedings in Computing, Volume 14, pages 6776, 2013, (pdf). [FM12] Hybrid: A Definitional Two Level Approach to Reasoning with HigherOrder Abstract Syntax, by Amy Felty and Alberto Momigliano. Journal of Automated Reasoning, 48(1):43105, 2012, DOI 10.1007/s108170109194x (SpringerLink, pdf). [MF11] An Improved Implementation and Abstract Interface for Hybrid, by Alan J. Martin, and Amy P. Felty. In Proceedings of the Sixth International Workshop on Logical Frameworks and MetaLanguages: Theory and Practice (LFMTP), August 2011, (pdf). [Mar10] Reasoning Using HigherOrder Abstract Syntax in a HigherOrder Logic Proof Environment: Improvements to Hybrid and a Case Study, by Alan J. Martin, Ph.D. thesis, University of Ottawa, November 2010 (pdf). [FP10] Reasoning with HigherOrder Abstract Syntax and Contexts: A Comparison, by Amy Felty and Brigitte Pientka. In International Conference on Interactive Theorem Proving, SpringerVerlag LNCS, July 2010 (pdf). [FM09] Reasoning with Hypothetical Judgments and Open Terms in Hybrid, by Amy Felty and Alberto Momigliano. In 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, September 2009 (pdf). [CF09] HigherOrder Abstract Syntax in Type Theory, by Venanzio Capretta and Amy Felty. In Logic Colloquium '06, ASL Lecture Notes in Logic, 32, Cambridge University Press, October 2009 (pdf). [MMF08] Twolevel Hybrid: A System for Reasoning Using HigherOrder Abstract Syntax, by Alberto Momigliano, Alan J. Martin, and Amy P. Felty. In Proceedings of the Second International Workshop on Logical Frameworks and MetaLanguages: Theory and Practice (LFMTP 2007), in Electronic Notes in Theoretical Computer Science, 196:8593, January 2008 (pdf) [CF07] Combining de Bruijn Indices and HigherOrder Abstract Syntax in Coq, by Venanzio Capretta and Amy Felty. In Types for Proofs and Programs, International Workshop, TYPES 2006, Revised Selected Papers, SpringerVerlag LNCS 4502, 2007 (pdf). [Fel02] TwoLevel MetaReasoning in Coq, by Amy P. Felty. In Fifteenth International Conference on Theorem Proving in Higher Order Logics, SpringerVerlag LNCS 2410, August 2002 (postscript). [DFH95] HigherOrder Abstract Syntax in Coq, by Joëlle Despeyroux, Amy Felty, and André Hirschowitz. In Second International Conference on Typed Lambda Calculi and Applications, SpringerVerlag LNCS 902, April 1995 (postscript). 