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, most recently tested with Coq Version 8.13.1.


Download

The Hybrid Libraries and Examples listed below can be downloaded as a single zip file.


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.v: The main syntax 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 [FMP18,FMP15a,FMP15b,FMP15c] for further information.


Other Experimental Versions of Hybrid in Coq

 
  • Hybrid as a linear logical framework applied to metatheory of quantum programming languages [MF18a,MF18b]
  • Hybrid with a more expressive specification logic that allows non-atomic formulas in contexts [BF16] (Coq formalization).
  • 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

 

    [FMP18] 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, 28:1507-1540, 2018, (pdf).

    [MF18a] Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic, by Mohamed Yousri Mahmoud and Amy P. Felty, 2018 (arXiv, pdf).

    [MF18b] Formal Meta-level Analysis Framework for Quantum Programming Languages, by Mohamed Yousri Mahmoud and Amy P. Felty. In Proceedings of the 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017), in Electronic Notes in Theoretical Computer Science, Volume 338, pages 185-201, 2018, (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 Meta-Languages: Theory and Practice (LFMTP), June 2016 (pdf).

    [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).