Recursion principles for syntax with bindings and substitution

Andrei Popescu, Elsa L. Gunter

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish (US)
Pages (from-to)346-358
Number of pages13
JournalACM SIGPLAN Notices
Issue number9
StatePublished - Sep 1 2011
Externally publishedYes


  • Lambda calculus
  • Recursion
  • Substitution
  • Syntax with bindings

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Recursion principles for syntax with bindings and substitution'. Together they form a unique fingerprint.

Cite this