Sciweavers

Share
ICFP
2005
ACM

A computational approach to reflective meta-reasoning about languages with bindings

9 years 7 months ago
A computational approach to reflective meta-reasoning about languages with bindings
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...
Aleksey Nogin, Alexei Kopylov, Xin Yu, Jason Hicke
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2005
Where ICFP
Authors Aleksey Nogin, Alexei Kopylov, Xin Yu, Jason Hickey
Comments (0)
books