Hybrid: Reasoning with Higher-Order Abstract Syntax in Coq and Isabelle

摘要

We present recent work on the Hybrid system [3, 5], a logical framework for specifying and reasoning about languages and deductive systems. One of the main areas of application of this system is developing formal proofs of properties of programming languages. It is well-known that those languages that are formally proven to be sound can better provide a solid basis for building software systems that are reliable and secure.rnHybrid is designed to exploit the advantages of higher-order abstract syntax within the well-understood setting of higher-order logic as implemented in a variety of general theorem proving systems. It is currently implemented in both Isabelle/HOL [6] and Coq[1].rnHybrid is definitional and introduces no new axioms. In particular, a de Bruijn representation of A-terms provides a definitional layer that allows the user to represent object languages using higher-order abstract syntax, while offering tools for reasoning about them at the higher level.rnWe describe a variety of features of Hybrid, including two-level reasoning [3] and inductive reasoning about open terms [4], and we present case studies to illustrate these features. We also discuss both classical and constructive [2] versions of Hybrid.