Abstract:

Verifying Explicit Substitution Calculi in Binding Structures with Effect Binding

Burkhart Wolff


Binding structures enrich traditional abstract syntax by provi-ding support for representing binding mechanisms 
(based on deBruijn indices), term-schemata and a very clean algebraic theory of substitution. Weprovide a novel 
binding structure with the following main results: 1) The formalisation of a generic binding structure with the 
novel conceptof effect-binding that enables the explicit representations of both contexts and terms inside one 
term meta-language,2) The foundation of a formal (machine-assisted) substitution theory of effect-binding that 
is well-suited for mechanisation. This can be used for thesystematic and correct development of new calculi with 
explicit substitutions.The substitution theory is formally proven in Isabelle/HOL; the implementation may serve 
as (untyped) framework for deep embeddings.