Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: The Nearly Ultimate Pearl
Authors: Constable, Robert L.
Bates, Joseph L.
Keywords: computer science
technical report
Issue Date: Jan-1983
Publisher: Cornell University
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.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
83-551.pdf3.12 MBAdobe PDFView/Open
83-551.ps761.82 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us