Recursive function definition for types with binders
Date
2004
Authors
Norrish, Michael
Journal Title
Journal ISSN
Volume Title
Publisher
Springer
Abstract
This work describes the proof and uses of a theorem allowing definition of recursive functions over the type of λ-calculus terms, where terms with bound variables are identified up to α-equivalence. The theorem embodies what is effectively a principle o
Description
Keywords
Citation
Collections
Source
Type
Book chapter
Book Title
Theorem Proving in Higher Order Logics: 17th international conference, TPHOLs 2004
Entity type
Access Statement
License Rights
DOI
Restricted until
2037-12-31