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...

• Type: Conference
• Year: 2005
• Where: ICFP
• Authors: Aleksey Nogin, Alexei Kopylov, Xin Yu, Jason Hickey
• Keywords: Computational Type Theory, General-purpose Type Theory, ICFP 2005, Programming Languages, Type Theory