Partial Objects in Type Theory
| dc.contributor.author | Smith, Scott Fraser | en_US |
| dc.date.accessioned | 2007-04-23T17:34:29Z | |
| dc.date.available | 2007-04-23T17:34:29Z | |
| dc.date.issued | 1988-08 | en_US |
| dc.description.abstract | Intuitionistic type theories, originally developed by Martin-Lof, provide a foundation for intuitionistic mathematics, much as set theory provides a foundation for mathematics. They are of interest to computer scientists because the objects typed are computations, making type theory an appropriate setting for reasoning about computation. Type theories such as Nuprl or the theories of Martin-Lof have types for objects that always terminate, but objects which may diverge are not directly typable. If type theory is to be a full-fledged theory for reasoning about computations, we need to be able to reason about potentially diverging objects. In this thesis we show how potentially diverging computations, which we call partial objects, may be typed by extending type theory to partial object type theory. New partial types are added to type partial objects. These types are usable: partial objects written in natural program notation can easily be shown to lie in the types. In addition to being able to express partial objects, it is also important to be able to reason about them; for this purpose general principles are given for proving facts about partial objects via induction. The resulting theory serves as a foundation for computational as well as mathematical reasoning. It also gives insights into abstract recursion theory, leads to a new method for constructive reasoning, and sheds light on inductive methods for reasoning about recursive computation. | en_US |
| dc.format.extent | 7330045 bytes | |
| dc.format.extent | 1239044 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.format.mimetype | application/postscript | |
| dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR88-938 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/6778 | |
| 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 | Partial Objects in Type Theory | en_US |
| dc.type | technical report | en_US |