@inproceedings{523a0e36f6234e9ca24141270a3213f5,
title = "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.",
keywords = "Lambda calculus, Recursion, Substitution, Syntax with bindings",
author = "Andrei Popescu and Gunter, {Elsa L.}",
year = "2011",
doi = "10.1145/2034773.2034819",
language = "English (US)",
isbn = "9781450308656",
series = "Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP",
pages = "346--358",
booktitle = "ICFP'11 - Proceedings of the 2011 ACM SIGPLAN International Conference on Functional Programming",
note = "16th ACM SIGPLAN International Conference on Functional Programming, ICFP'11 ; Conference date: 19-09-2011 Through 21-09-2011",
}