Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/6391
 Title: The Nearly Ultimate Pearl Authors: Constable, Robert L.Bates, Joseph L. Keywords: computer sciencetechnical report Issue Date: Jan-1983 Publisher: Cornell University Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR83-551 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. URI: http://hdl.handle.net/1813/6391 Appears in Collections: Computer Science Technical Reports

Files in This Item:

File Description SizeFormat