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
model is
 representationally adequate for HOAS. The proof is quite technical
 in nature, so the talk will focus on an explanation of the key
 ideas.

 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.