A Computational Approach to Reflective Meta-Reasoning about Languages with Bindings

Nogin, Aleksey and Kopylov, Alexei and Xin, Yu and Hickey, Jason (2005) A Computational Approach to Reflective Meta-Reasoning about Languages with Bindings. In: MERλIN 2005. ICFP 2005 Workshop on MEchanized Reasoning about Languages with variable biNding, September 30, 2005, Tallinn, Estonia.

Full text available as:

	PDF - Requires Adobe Acrobat Reader or other PDF viewer.
	Postscript - Requires a viewer, such as GhostView

Abstract

We present a foundation for a computational meta-theory of languages with bindings implemented in a computer-aided formal reasoning environment. Our theory provides the ability to reason abstractly about operators, languages, open-ended languages, classes of languages, etc. The theory is based on the ideas of higher-order abstract syntax, with an appropriate induction principle parameterized over the language (i.e. a set of operators) being used. In our approach, both the bound and free variables are treated uniformly and this uniform treatment extends naturally to variable-length bindings. The implementation is reflective, namely there is a natural mapping between the meta-language of the theorem-prover and the object language of our theory. The object language substitution operation is mapped to the meta-language substitution and does not need to be defined recursively. Our approach does not require designing a custom type theory; in this paper we describe the implementation of this foundational theory within a general-purpose type theory. This work is fully implemented in the MetaPRL theorem prover, using the pre-existing NuPRL-like Martin-Lof-style computational type theory. Based on this implementation, we lay out an outline for a framework for programming language experimentation and exploration as well as a general reflective reasoning framework. This paper also includes a short survey of the existing approaches to syntactic reflection.

EPrint Type:	Conference or Workshop Item (Paper)
Uncontrolled Keywords:	Higher-Order Abstract Syntax, Reflection, Type Theory, MetaPRL, NuPRL, Programming Language Experimentation, Languages with Bindings.
Subjects:	All Records
ID Code:	547
Deposited By:	Aleksey Nogin
Deposited On:	21 July 2005
Record Number:	CaltechCSTR:2005.003
Official Persistent URL:	http://resolver.caltech.edu/CaltechCSTR:2005.003
Usage Policy:	This is an extended version of the paper accepted to the MERLIN'05 Workshop (September 30, 2005, Tallinn, Estonia). The MERLIN paper is Copyright (C) 2005 ACM 1-59593-072-8/05/0009. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee.

Archive Staff Only: edit this record