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