Recursive function definition for types with binders
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
|Collections||ANU Research Publications|
|01_Norrish_Recursive_function_definition_2004.pdf||130.29 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.