Aaron, Eric2023-05-222023-05-222001-01-012008-01-17https://repository.upenn.edu/handle/20.500.14332/7782This document is intended to introduce the key elements of the Nuprl Proof Development System (Nuprl, for short) from the perspective of a Nuprl user, as opposed to the perspective of someone intimately involved in developing or extending Nuprl. As such, it may be more appropriate than other Kuprl-related documents for readers who are primarily concerned with uses of Nuprl and not fine details of Nuprl's mathematical foundation. It introduces and illustrates key Kuprl concepts -such as types, terms, displayforms, and tactics - in the framework of a model of calculational predicate logic inference.Report