Show simple item record

dc.contributor.authorConstable, Robert L.en_US
dc.contributor.authorBates, Joseph L.en_US
dc.description.abstractThe 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.extent3192428 bytes
dc.format.extent780108 bytes
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleThe Nearly Ultimate Pearlen_US
dc.typetechnical reporten_US

Files in this item


This item appears in the following Collection(s)

Show simple item record