dc.contributor.author Constable, Robert L. en_US dc.contributor.author Bates, Joseph L. en_US dc.date.accessioned 2007-04-23T16:47:39Z dc.date.available 2007-04-23T16:47:39Z dc.date.issued 1983-01 en_US dc.identifier.citation http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR83-551 en_US dc.identifier.uri https://hdl.handle.net/1813/6391 dc.description.abstract The PRL ("pearl") system is an environment providing computer assistance in the construction of formal proofs and programs in a particular formal theory, called the object theory. Certain proofs can in fact be considered as programs. The system embodies knowledge about programs in the form of rules of inference and in the form of facts stored in its library. Ultimately PRL may be regarded as an intelligent system for formal constructive problem solving in a large domain of mathematics. The PRL system is evolving in stages. Since our report "The Definition of Micro-PRL" in October 1981, we have had the experience of designing, building and using a complete core version of the system (called $\lambda$PRL). We have also studied more deeply the theoretical issues raised in that report. We are now prepared to extend the core system closer to the "ultimate" PRL system envisioned earlier. This document describes the mathematical theory of types which is the object theory of that extension (called $\lambda$PRL) and it is more or less self-contained. The type theory is defined in stages, starting from a constructive theory of integers and lists ("PRL). The development is a main feature of the paper. en_US dc.format.extent 3192428 bytes dc.format.extent 780108 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 The Nearly Ultimate Pearl en_US dc.type technical report en_US
﻿