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...

• Type: Conference
• Year: 2009
• Where: PPDP
• Authors: Amy P. Felty, Alberto Momigliano
• Keywords: Abstract Syntax, Inference Rules, PPDP 2009, Programming Languages