CaltechTHESIS
  A Caltech Library Service

Reflection and its application to mechanized metareasoning about programming languages

Citation

Yu, Xin (2007) Reflection and its application to mechanized metareasoning about programming languages. Dissertation (Ph.D.), California Institute of Technology. http://resolver.caltech.edu/CaltechETD:etd-05222007-211909

Abstract

It is well known that adding reflective reasoning can tremendously increase the power of a proof assistant. In order for this theoretical increase of power to become accessible to users in practice, the proof assistant needs to provide a great deal of infrastructure to support reflective reasoning. In this thesis we explore the problem of creating a practical implementation of such a support layer. Our implementation takes a specification of a logical theory (which is identical to how it would be specified if we simply intended to reason within this logical theory, instead of reflecting it) and automatically generates the necessary definitions, lemmas, and proofs that are needed to enable the reflected metareasoning in the provided theory. One of the key features of our approach is that the structure of a logic 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 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:Thesis (Dissertation (Ph.D.))
Subject Keywords:formal reasoning; MetaPRL; metareasoning; reflective reasoning
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Computer Science
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Hickey, Jason J.
Thesis Committee:
  • Hickey, Jason J. (chair)
  • Martin, Alain J.
  • Joshi, Rajeev
  • Low, Steven H.
Defense Date:12 June 2006
Record Number:CaltechETD:etd-05222007-211909
Persistent URL:http://resolver.caltech.edu/CaltechETD:etd-05222007-211909
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:1960
Collection:CaltechTHESIS
Deposited By: Imported from ETD-db
Deposited On:30 May 2007
Last Modified:26 Dec 2012 02:44

Thesis Files

[img]
Preview
PDF (thesis_xin.pdf) - Final Version
See Usage Policy.

712Kb

Repository Staff Only: item control page