Back to my publications
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.
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.
Last update: Saturday, January 27, 2007 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)