CaltechAUTHORS
  A Caltech Library Service

Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection

Hickey, Jason and Nogin, Aleksey and Yu, Xin and Kopylov, Alexei (2006) Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection. ACM SIGPLAN Notices, 41 (9). pp. 172-183. ISSN 0362-1340. doi:10.1145/1160074.1159826. https://resolver.caltech.edu/CaltechAUTHORS:20161103-125705148

Full text is not posted in this repository. Consult Related URLs below.

Use this Persistent URL to link to this item: https://resolver.caltech.edu/CaltechAUTHORS:20161103-125705148

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 (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.


Item Type:Article
Related URLs:
URLURL TypeDescription
http://dx.doi.org/10.1145/1160074.1159826DOIArticle
http://dl.acm.org/citation.cfm?doid=1160074.1159826PublisherArticle
Additional Information:© 2006 ACM.
Subject Keywords:Languages, Theory, Verification, Reflection, Higher-Order Abstract Syntax, Meta-Theory, Type Theory, MetaPRL, NuPRL, Languages with Bindings, Mechanized Reasoning
Issue or Number:9
Classification Code:F.4.3 [ Mathematical Logic and Formal Languages ]: Formal Languages—Operations on lan- guages; F.4.1 [ Mathematical Logic and Formal Languages ]: Math- ematical Logic—Mechanical theorem proving; D.3.1 [ Program- ming Languages ]: Formal Definitions and
DOI:10.1145/1160074.1159826
Record Number:CaltechAUTHORS:20161103-125705148
Persistent URL:https://resolver.caltech.edu/CaltechAUTHORS:20161103-125705148
Official Citation:Jason Hickey, Aleksey Nogin, Xin Yu, and Alexei Kopylov. 2006. Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection. SIGPLAN Not. 41, 9 (September 2006), 172-183. DOI=http://dx.doi.org/10.1145/1160074.1159826
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:71711
Collection:CaltechAUTHORS
Deposited By: Kristin Buxton
Deposited On:03 Nov 2016 23:58
Last Modified:11 Nov 2021 04:49

Repository Staff Only: item control page