dc.contributor.author Constable, Robert L. en_US dc.contributor.author Mendler, N. P. en_US dc.date.accessioned 2007-04-23T17:08:03Z dc.date.available 2007-04-23T17:08:03Z dc.date.issued 1985-01 en_US dc.identifier.citation http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR85-659 en_US dc.identifier.uri https://hdl.handle.net/1813/6499 dc.description.abstract The type theories we consider are adequate for the foundations of mathematics and computer science. Recursive type definitions are important practical ways to organize data, and they express powerful axioms about the termination of procedures. In the theory examined here, the demands of practicality arising from our implemented system, Nuprl, suggest an approach to recursive types that significantly increases the proof theoretic power of the theory and leads to insights into computational semantics. We offer a new account of recursive definitions for both types and partial functions. The computational requirements of the theory restrict recursive type definitions involving the total function-space constructor ($\rightarrow$) to those with only positive occurrences of the defined type. But we show that arbitrary recursive definitions with respect to the partial function-space constructor are sensible. The partial function-space constructor allows us to express reflexive types of Scott's domain theory (as needed to model the lambda calculus) and thereby reconcile parts of domain theory with constructive type theory. en_US dc.format.extent 2271289 bytes dc.format.extent 575366 bytes dc.format.mimetype application/pdf dc.format.mimetype application/postscript dc.language.iso en_US en_US dc.publisher Cornell University en_US dc.subject computer science en_US dc.subject technical report en_US dc.title Recursive Definitions in Type Theory en_US dc.type technical report en_US
﻿