Hybrid Representational Adequacy
Hybrid is a logical Framework introduced by Ambler, Crole and
Momigliano. Implemented within Isabelle HOL, it allows object logics
to be represented using higher order abstract syntax (HOAS), and
reasoned about using tactical theorem proving in general and
principles of (co)induction in particular.
Of fundamental interest is the form of the lambda abstractions
provided by Hybrid. The user has the convenience of writing lambda
abstractions using names for the binding variables. However each
abstraction is actually a definition of a de Bruijn
expression, and Hybrid can unwind the user's abstractions (written
with names) to machine friendly de Bruijn expressions (without
names). In this sense the formal system contains a Hybrid of
named and nameless bound variable notation.
We present a mathematical model of Hybrid, and sketch a proof that the
representationally adequate for HOAS. The proof is quite technical
in nature, so the talk will focus on an explanation of the key
The adequacy result requires a detailed proof that proper locally
nameless de Bruijn expressions and alpha-equivalence classes of
lambda-expressions are in bijective correspondence. This result
is presented as a form of de Bruijn representational adequacy, and
is a key component of the proof of Hybrid adequacy.