Canonical HybridLF: Extending Hybrid with Dependent Types

We introduce Canonical HybridLF (CHLF), a metalogic for proving properties of deductive systems, implemented in Isabelle HOL. CHLF is closely related to two other metalogics. The first is the Edinburgh Logical Framework (LF) by Harper, Honsell and Plotkin. The second is the Hybrid system developed by Ambler, Crole and Momigliano which provides a Higher-Order Abstract Syntax (HOAS) based on un-typed lambda calculus. Historically there are two problems with HOAS: its incompatibility with inductive types and the presence of exotic terms. Hybrid provides a partial solution to these problems whereby HOAS functions that include bound variables in the metalogic are automatically converted to a machine-friendly de Bruijn representation hidden from the user. The key innovation of CHLF is the replacement of the un-typed lambda calculus with a dependently-typed lambda calculus in the style of LF. CHLF allows signatures containing constants representing the judgements and syntax of an object logic, together with proofs of metatheorems about its judgements, to be entered using a HOAS interface. Proofs that metatheorems defined in the signature are valid are created using the M2 metalogic of Schurmann and Pfenning. We make a number of advances over existing versions of Hybrid: we now have the utility of dependent types; the unitary bound variable capability of Hybrid is now potentially finitary; a type system performs the role of Hybrid well-formedness predicates; and the old method of indicating errors using special elements of core datatypes is replaced with a more streamlined one that uses the Isabelle option type.