Two-level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax

The Hybrid System in Coq

Hybrid is a system designed for reasoning using higher-order abstract syntax representations of object logics. It is implemented in both Isabelle and Coq. This page describes the Coq version. Other information on Hybrid can be found here.


Hybrid Libraries

Hybrid implements a definitional, multi-level approach. In particular, higher-order syntax encodings are defined on top of the base level so that they expand to a de Bruijn representation of terms. The Hybrid package provides a library of operations and lemmas to reason on this higher-order syntax, while hiding the details of the de Bruijn representation.

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.
 
  • Hybrid.v: The main library
  • sl.v: Example specification logic (fragment of 2nd-order minimal logic)


Examples


ORBI Benchmarks

Some of the examples above appear as solutions to the ORBI (Open Challenge problem Repository for systems supporting reasoning with Binders) benchmark problems. See the hybrid subdirectory in the solutions directory in the repository. See also [FMP15a,FMP15b,FMP15c] for further information.


Download

The Hybrid libraries plus all the examples listed above can be downloaded as a single gzipped tar file.


Other Experimental Versions of Hybrid in Coq

 
  • A constructive version of Hybrid in Coq, which includes recursion principles that work directly on higher-order syntax is described in [CF07] (Coq formalization).
  • A generalized version of the above, where a large class of theorems that must be repeated for each object language in Hybrid is done once in the new version and can be applied directly to each object language, is described in [CF09] (Coq formalization, example application).

References

 

    [FMP15a] The Next 700 Challenge Problems for Reasoning with Higher-Order 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 Higher-Order 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 Meta-Languages: Theory and Practice (LFMTP), in Electronic Proceedings in Theoretical Computer Science, Volume 185, pages 18-32, August 2015 (pdf).

    [HF13] Translating Higher-Order 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 67-76, 2013, (pdf).

    [FM12] Hybrid: A Definitional Two Level Approach to Reasoning with Higher-Order Abstract Syntax, by Amy Felty and Alberto Momigliano. Journal of Automated Reasoning, 48(1):43-105, 2012, DOI 10.1007/s10817-010-9194-x (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 Meta-Languages: Theory and Practice (LFMTP), August 2011, (pdf).

    [Mar10] Reasoning Using Higher-Order Abstract Syntax in a Higher-Order 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 Higher-Order Abstract Syntax and Contexts: A Comparison, by Amy Felty and Brigitte Pientka. In International Conference on Interactive Theorem Proving, Springer-Verlag 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] Higher-Order 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] Two-level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax, by Alberto Momigliano, Alan J. Martin, and Amy P. Felty. In Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007), in Electronic Notes in Theoretical Computer Science, 196:85-93, January 2008 (pdf)

    [CF07] Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq, by Venanzio Capretta and Amy Felty. In Types for Proofs and Programs, International Workshop, TYPES 2006, Revised Selected Papers, Springer-Verlag LNCS 4502, 2007 (pdf).

    [Fel02] Two-Level Meta-Reasoning in Coq, by Amy P. Felty. In Fifteenth International Conference on Theorem Proving in Higher Order Logics, Springer-Verlag LNCS 2410, August 2002 (postscript).

    [DFH95] Higher-Order Abstract Syntax in Coq, by Joëlle Despeyroux, Amy Felty, and André Hirschowitz. In Second International Conference on Typed Lambda Calculi and Applications, Springer-Verlag LNCS 902, April 1995 (postscript).