Recursion principles for syntax with bindings and substitution

Andrei Popescu, Elsa L. Gunter

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationICFP'11 - Proceedings of the 2011 ACM SIGPLAN International Conference on Functional Programming
Pages346-358
Number of pages13
DOIs
StatePublished - 2011
Event16th ACM SIGPLAN International Conference on Functional Programming, ICFP'11 - Tokyo, Japan
Duration: Sep 19 2011Sep 21 2011

Publication series

NameProceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP

Other

Other16th ACM SIGPLAN International Conference on Functional Programming, ICFP'11
Country/TerritoryJapan
CityTokyo
Period9/19/119/21/11

Keywords

  • Lambda calculus
  • Recursion
  • Substitution
  • Syntax with bindings

ASJC Scopus subject areas

  • Software

Fingerprint

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

Cite this