cms

Combining HOAS with Induction and Coinduction

Associated Researchers: Dr. R. L. Crole
Research Collaborator: Dr. A. Momigliano

Many people are concerned with the development of computing systems which can be used to reason about and prove properties of programming languages. However, developing such systems is not easy. Difficulties abound in both practical implementation and underpinning theory. Some of our recent work makes both a theoretical and practical contribution to this research area. More precisely, the work concerns how to reason about object level logics with syntax involving variable binding---note that a programming language can be presented as an example of such an object logic.

What are the key issues here? It is well known that it is not easy to generate computer representations of such object level binding logics. A major problem is that there are certain meta-level operations, such as substitution, which operate on each logic. These operations must be re-implemented for each new object logic, which is very time consuming. One approach to this problem is the use of so-called Higher Order Abstract Syntax. Roughly speaking, HOAS is a form of metalanguage, in which such meta-level operations are encoded, once and for all. The object level logics are then each translated into HOAS, and the translations are reasoned about.

What kind of reasoning is used? Typically the translation is reasoned about by using induction and coinduction. However, it is well known that combining HOAS and induction can lead to inconsistencies, and a good deal of theory has already been developed which explains why this can happen. We have shown in our work, that with very careful handling of some central technical issues, it is possible to combine HOAS and induction. In fact our work has lead to the development of a mechanized tool, HYBRID2, which has been coded within Isabelle HOL, and

• provides a form of logical framework within which the syntax of an object level logic can be adequately represented by higher order abstract syntax (HOAS);
• is consistent with tactical theorem proving in general, and principles of induction and coinduction in particular; and
• is definitional which guarantees consistency within a classical type theory.

A description of this work, along with some simple applications, can be found in the paper Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction. In Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, Hampton, VA, USA, volume 2410 of Lecture Notes in Computer Science, pages 13-30. Springer-Verlag, 2002.
[ bib | .ps.gz ]

Author: R. L. Crole (R.Crole at mcs.le.ac.uk), T: +44 (0)116 252 3404 .
© University of Leicester February 2003. Last modified: 4th May 2005, 10:10:57
CMS Web Maintainer. This document has been approved by the Head of Department.