Skip navigation
Skip navigation

Recursive function definition for types with binders

Norrish, Michael


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

CollectionsANU Research Publications
Date published: 2004
Type: Book chapter


File Description SizeFormat Image
01_Norrish_Recursive_function_definition_2004.pdf130.29 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator