Two-Level Hybrid in Coq: Benchmarks

Software Correctness and Safety Research Laboratory
School of Information Technology and Engineering
University of Ottawa

This page is superseded by this one, but serves as a stand-alone electronic appendix for the Hybrid versions of the benchmarks described in [FP10]. The Twelf and Beluga versions are available here.


Hybrid Libraries

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


References

 

    [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, 2015, Journal of Automated Reasoning, to appear (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).