**Alberto Momigliano**

University of Leicester
###
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and
(Co)Induction

Abstract:
Combining Higher Order Abstract Syntax (HOAS) and (co)induction is well
known to be problematic. We have implemented a tool called Hybrid,
within Isabelle HOL, which does allow object logics to be represented using
HOAS, and reasoned about using tactical theorem proving in general and
principles of (co)induction in particular. Moreover, it is definitional,
which guarantees consistency within a classical type theory. The basic
idea is that the HOAS meta-language is only a notation for a traditional
de Bruijn style encoding; however, the user level is separated from that
infrastructure. The latter provides a number of theorems and tactics which
allows one to work with (co)inductive notions over HOAS specifications.

In this talk we describe Hybrid and compare it with other systems.
We also provide some theoretical adequacy results which underpin our practical
work. As a case study, we illustrate the use of Hybrid for reasoning
about the lazy \lambda-calculus. In particular, we present a formal
verification that the Abramsky's notion of (bi)simulation is a (pre)congruence,
using Howe's technique.

Joint work with S.J. Ambler & R.L. Crole

Host: Frank Pfenning

Appointments: Rae Graham

Principles
of Programming Seminars

POP Seminar

May 10, 2002

3:30 p.m.

Wean Hall 8220