HybridLF: a system for reasoning in higher-order abstract syntax

In this thesis we describe two new systems for reasoning about deductive systems: HybridLF and Canonical HybridLF. HybridLF brings together the Hybrid approach (due to Ambler, Crole and Momigliano [15]) to higher-order abstract syntax (HOAS) in Isabelle/HOL with the logical framework LF, a dependently-typed system for proving theorems about logical systems. Hybrid provides a version of HOAS in the form of the lambda calculus, in which Isabelle functions are automatically converted to a nameless de Bruijn represenation. Hybrid allows untyped expressions to be entered as human-readable functions, which are then translated into the machine-friendly de Bruijn form. HybridLF uses and updates these techniques for variable representation in the context of the dependent type theory LF, providing a version of HOAS in the form of LF. Canonical HybridLF unites the variable representation techniques of Hybrid with Canonical LF, in which all terms are in canonical form and definitional equality is reduced to syntactic equality. We extend the Hybrid approach to HOAS to functions with multiple variables by introducing a family of abstraction functions, and use the Isabelle option type to denote errors instead of including an ERR element in the Canonical HybridLF expression type. In both systems we employ the meta-logic M2 to prove theorems about deductive systems. M2 [28] is a first-order logic in which quantifiers range over the objects and types generated by an LF signature (that encodes a deductive system). As part of the implementation of M2 we explore higher-order unification in LF, adapting existing approaches to work in our setting.