recursion principles for syntax with bindings and substitution
We characterize the data type of terms with bindings, freshness and substitution, as an initial model in a suitable Horn theory. This characterization yields a convenient recursive definition principle, which we have formalized in Isabelle/HOL and employed in a series of case studies taken from the ?-calculus literature.
recursion syntax with bindings substitution lambda calculus