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
Type | Conference paper |
---|---|
Title | Recursion principles for syntax with bindings and substitution |
Authors | Popescu, 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 Group | Foundations of Computing group |
Conference | The 16th ACM SIGPLAN International Conference on Functional Programming |
Page range | 346-358 |
ISBN | |
Hardcover | 9781450308656 |
Publisher | Association for Computing Machinery (ACM) |
Publication dates | |
Sep 2011 | |
Publication process dates | |
Deposited | 23 Apr 2015 |
Output status | Published |
Web address (URL) | http://dx.doi.org//10.1145/2034773.2034819 |
Language | English |
Book title | Proceedings of the 16th ACM SIGPLAN international conference on Functional programming |
Permalink -
https://repository.mdx.ac.uk/item/8511y
19
total views0
total downloads0
views this month0
downloads this month