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 (submitted), University of Ottawa, January 2010. [code]
A. Felty and A.M. 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. Felty and A. Momigliano. Hybrid: a Definitional Two-Level Approach to Reasoning with Higher Order Abstract syntax. This is a comprehensive summary of Hybrid and has been submitted to a journal, September 2008. Avaliable as a University of Ottawa Tech Report, number TR-2008-03. [PDF] [code]
A. Momigliano, A. Martin and A. Felty. Two-level Hybrid: A System for Reasoning using HOAS. [PDF]. LFMTP 2007, August 2007. Appeared in 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]

Please, refer to this page.

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