# Hybrid Representational Adequacy

- 14:00 2nd December 2011 ( week 8, Michaelmas Term 2011 )380

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.