Recursion principles for syntax with bindings and substitution

Abstract

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.