Nogin, Aleksey and Kopylov, Alexei and Xin, Yu and Hickey, Jason (2005) A Computational Approach to Reflective Meta-Reasoning about Languages with Bindings. . (In Press) http://resolver.caltech.edu/CaltechCSTR:2005.003
See Usage Policy.
See Usage Policy.
Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechCSTR:2005.003
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.
|Item Type:||Report or Paper (Technical Report)|
|Group:||Computer Science Technical Reports|
|Subject Keywords:||Higher-Order Abstract Syntax, Reflection, Type Theory, MetaPRL, NuPRL, Programming Language Experimentation, Languages with Bindings.|
|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.|
|Deposited By:||Imported from CaltechCSTR|
|Deposited On:||21 Jul 2005|
|Last Modified:||26 Dec 2012 14:14|
Repository Staff Only: item control page