The Nearly Ultimate Pearl

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