# Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and
reflection.

Jason Hickey, Aleksey Nogin, Xin Yu, and Alexei Kopylov

**Mechanized meta-reasoning using a hybrid HOAS/de Bruijn
representation and reflection.**

In John H. Reppy and Julia L. Lawall, editors, *Proceedings
of the 11th ACM SIGPLAN International Conference on Functional Programming,
ICFP 2006*, pages 172–183. ACM, 2006.

ACM Digital Library
Entry,
PDF.

## Abstract

We investigate the development of a general-purpose framework for
mechanized reasoning about the meta-theory of programming languages.
In order to provide a standard, uniform account of a programming language,
we propose to define it as a logic in a logical framework, using the same
mechanisms for definition, reasoning, and automation that are available to
other logics. Then, in order to reason about the language's meta-theory,
we use reflection to inject the programming language into a (usually
richer and more expressive) meta-theory.
One of the key features of our approach is that structure of the language
is preserved when it is reflected, including variables, meta-variables,
and binding structure. This allows the structure of proofs to be
preserved as well, and there is a one-to-one map from proof steps in
the original programming logic to proof steps in the reflected logic.
The act of reflecting a language is automated; all definitions, theorems,
and proofs are preserved by the transformation and all the key lemmas
(such as proof and structural induction) are automatically derived.

The principal representation used by the reflected logic is higher-order
abstract syntax (HOAS). However, reasoning about terms in HOAS can be
awkward in some cases, especially for variables. For this reason, we
define a computationally equivalent variable-free de Bruijn representation
that is interchangeable with the HOAS in all contexts. The de Bruijn
representation inherits the properties of substitution and alpha-equality
from the logical framework, and it is not complicated by administrative
issues like variable renumbering.

We further develop the concepts and principles of proofs, provability,
and structural and proof induction. This work is fully implemented in
the MetaPRL theorem prover. We illustrate with an application to
`F`_{<:} as defined in the POPLmark challenge.

Back to my publications

Last update: Saturday, January 27, 2007 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)