Combining Higher Order Abstract Syntax (HOAS) and (co)induction is well known to be problematic.  In previous work~\cite{Ambler02} we have described the implementation of a tool called Hybrid, within  Isabelle HOL, which allows object logics to be represented using  HOAS, and reasoned about using tactical theorem proving and  principles of (co)induction.  Moreover, it is definitional, which  guarantees consistency within a classical type theory.  In this  paper we describe how to use it in a multi-level reasoning fashion,  similar in spirit to other meta-logics such $\foldn$ and  \emph{Twelf}. By explicitly referencing provability, we solve the  problem of reasoning by (co)induction in presence of  non-stratifiable hypothetical judgments, which allow very elegant  and succinct specifications. We demonstrate the method by formally  verifying the correctness of a compiler for (a fragment) of Mini-ML,  following~\cite{Hannan92lics}. To further exhibit the flexibility of  our system, we modify the target language with a notion of  non-well-founded closure, inspired by Milner \&  Tofte~\cite{milner91d} and formally verify via coinduction a subject  reduction theorem for this modified language.

• Compiler verification with fix points (FIXC)
• Subject reduction with non-well founded closures (MT)