Show simple item record

dc.contributor.authorConstable, Robert L.en_US
dc.contributor.authorMendler, N. P.en_US
dc.description.abstractThe 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.extent2271289 bytes
dc.format.extent575366 bytes
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleRecursive Definitions in Type Theoryen_US
dc.typetechnical reporten_US

Files in this item


This item appears in the following Collection(s)

Show simple item record