Hybrid: a package for higher-order syntax in Isabelle and Coq

A. Martin. Reasoning Using Higher-Order Abstract Syntax in a Higher-Order Logic Proof Environment: Improvements to Hybrid and a Case Study. Ph. D. thesis, University of Ottawa, November 2010. [PDF] [code]
A.Felty and B.Pientka. Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. ITP 2010. July 2010. [DOI] [web page].
A. Felty and A. Momigliano. Hybrid: a Definitional Two-Level Approach to Reasoning with Higher Order Abstract Syntax. Journal of Automated Reasoning, July 2010. [DOI] [code] This is a comprehensive summary of Hybrid.
A. Felty and A. Momigliano. Reasoning with Hypothetical Judgments and Open Terms in Hybrid. PPDP 2009. [PDF] [code]
A. Martin. Case Study: Subject Reduction for Mini-ML with References, in Isabelle/HOL + Hybrid. 3rd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory, Victoria, British Columbia, Canada, 20 September 2008. [slides]
A. Momigliano., A. Martin and A. Felty. Two-level Hybrid: A System for Reasoning using HOAS. [PDF]. LFMTP 2007, August 2007. ENTCS, Volume 196, Pages 85-93. (22 Jan 2008).
A. Felty. Higher-Order Abstract Syntax, de Bruijn Terms, and Two-Level Reasoning in Coq and Isabelle. Invited talk at TYPES 2007, 2-5 May 2007. Cividale del Friuli (Udine), Italy. [slides]
Venanzio Capretta, Amy Felty: Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq. TYPES 2006:63-77
Amy Felty: Two-Level Meta-reasoning in Coq. TPHOLs 2002:198-213

Please, refer to this page.

The project is supported in part by the Natural Sciences and Engineering Research Council of Canada.

[ Home | Publications | JAR | Links ]