The talk will be divided in two parts. In the first one, joint work with Amy Felty (Ottawa), we describe the new version of Hybrid, a system for reasoning using higher-order syntax in theorem proving systems such as Coq and Isabelle. This is a refinement of Miller et al. "two-level approach", where the representation and the reasoning over deductive systems is split into different levels so as to avoid the usual incompatibility of HOAS and inductive definitions (types). We exemplify the approach with the verification of properties of continuation machines with a ordered linear logic frameworks.

In the second part, joint work with James Cheney (LFCS), we investigate the dual problem of searching for errors in formalized systems, such as programming language calculi, type systems, operational semantics etc. We consider the problem of bounded model-checking for meta-theoretic properties of formal systems specified using logical framework such as nominal logic, although this can be applied to other logical frameworks, like Twelf. In contrast to the current state of the art for metatheory verification, our approach is fully automatic, does not require expertise in theorem proving on the part of the user, and produces counterexamples in the case that a flaw is detected. We present two implementations of this technique, one based on negation-as-failure and one based on negation elimination. These techniques seem fast enough to be used interactively to debug systems as they are developed.