A Theory of Generic Binding-Structures and Substitutions

Burkhart Wolff
University of Bremen - FB 3, Germany

Starting with a critique of C. Talcott's work on Binding-Structures (TCS 93), I will present a generic data structure with meta-variables and variable binding. A substantial novelty herein is the concept of Effect-Binding. The data structure (plus its substitution theory) is developed as a conservative extension in Isabelle HOL. Some example encodings were presented.

This reports ongoing work.