Acronyms

Acronyms

    In 1979, the name "PRL" stood for Program Refinement Logic, but nowadays we think of it as Proof Refinement Logic. According to the proofs-as-programs principle, the names are equivalent in some sense. We designed and built several "PRL" systems. The first was LambdaPRL, then a microPRL and then began a series of systems called Nuprl, pronounced "new pearl." This was version "nu" of the PRL systems. Sometimes it is written NuPRL or NuPrl to show this origin, but the name Nuprl also plays on the notion of a "new" kind of system.