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.