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

MERLIN 2005

数学;计算机科学

Aleksey Nogin ; Alexei Kopylov ; Xin Yu ; Jason Hickey

Others  :  http://homepages.inf.ed.ac.uk/rpollack/TYPES/MERLIN_05/p2-nogin.pdf
PID  :  52664

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

We present a foundation for a computational meta-theory of lan- guages with bindings implemented in a computer-aided formal rea- soning environment. Our theory provides the ability to reason ab- stractly 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 parameter- ized over the language (i.e. a set of operators) being used. In our ap- proach, both the bound and free variables are treated uniformly and this uniform treatment extends naturally to variable-length bind- ings. 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 op- eration is mapped to the meta-language substitution and does not need to be defined recursively. Our approach does not require de- signing a custom type theory; in this paper we describe the im- plementation of this foundational theory within a general-purpose type theory. This work is fully implemented in the MetaPRL the- orem prover, using the pre-existing NuPRL-like Martin-Lo¨f-style computational type theory. Based on this implementation, we lay out an outline for a framework for programming language experi- mentation and exploration as well as a general reflective reasoning framework. This paper also includes a short survey of the existing approaches to syntactic reflection. Categories and Subject Descriptors D.3.1 [Programming Lan- guages]: Formal Definitions and Theory—Syntax; F.4.3 [Math- ematical Logic and Formal Languages]: Formal Languages— Operations on languages General Terms Languages, Theory, Verification