Reasoning with hypothetical judgments and open terms in hybrid

9 years 5 months ago
Reasoning with hypothetical judgments and open terms in hybrid
Hybrid is a system developed to specify and reason about logics, programming languages, and other formal systems expressed in rder abstract syntax (HOAS). An important goal of Hybrid is to exploit the advantages of HOAS within the well-understood setting of higher-order logic as implemented by systems such as Isabelle and Coq. In this paper, we add new capabilities for reasoning by induction on encodings of object-level inference rules. Elegant and succinct specifications of such inference rules can often be given using hypothetical and parametric judgments, which are represented by embedded implication and universal quantification. Induction over such judgments is well-known to be problematic. In previous work, we showed how to express this kind of judgment using a two-level approach, but reasoning by induction on such judgments was restricted to closed terms. The new capabilities we add include techniques for adding arbitrary “new” variables to contexts and inductively reasoni...
Amy P. Felty, Alberto Momigliano
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where PPDP
Authors Amy P. Felty, Alberto Momigliano
Comments (0)