Skip navigation
Skip navigation

Recursive function definition for types with binders

Norrish, Michael

Description

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
URI: http://hdl.handle.net/1885/87609

Download

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:  23 August 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator