Recursion principles for syntax with bindings and substitution

Conference paper

Popescu, A. and Gunter, E. 2011. Recursion principles for syntax with bindings and substitution. The 16th ACM SIGPLAN International Conference on Functional Programming. Tokyo 19 - 21 Sep 2011 Association for Computing Machinery (ACM). pp. 346-358
TypeConference paper
TitleRecursion principles for syntax with bindings and substitution
AuthorsPopescu, A. and Gunter, E.
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

Research GroupFoundations of Computing group
ConferenceThe 16th ACM SIGPLAN International Conference on Functional Programming
Page range346-358
ISBN
Hardcover9781450308656
PublisherAssociation for Computing Machinery (ACM)
Publication dates
PrintSep 2011
Publication process dates
Deposited23 Apr 2015
Output statusPublished
Web address (URL)http://dx.doi.org//10.1145/2034773.2034819
LanguageEnglish
Book titleProceedings of the 16th ACM SIGPLAN international conference on Functional programming
Permalink -

https://repository.mdx.ac.uk/item/8511y

Log in to edit
  • 21
    total views
  • 0
    total downloads
  • 2
    views this month
  • 0
    downloads this month

Export as