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 higher-order 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 reasoning about open terms. Very little overhead is required, namely a small library of definitions and lemmas, yet the reasoning power of the system and the class of properties that can be proved is significantly increased. We illustrate the approach using PCF, a simple programming language that serves as the core of a variety of functional languages. We encode the typing judgment, and prove by induction on this judgment that well-typed PCF terms have unique types.