Now showing items 1-6 of 6

• #### The Definition of $\mu$PRL ﻿

(Cornell University, 1982-10)
NO ABSTRACT SUPPLIED
• #### A Logic for Correct Program Development ﻿

(Cornell University, 1981-03)
Existing verification technology, though theoretically adequate, is not directly applicable to the construction of large software systems. This thesis explores the view that reasoning about code is not the proper paradigm ...
• #### The Nearly Ultimate Pearl ﻿

(Cornell University, 1983-01)
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 ...
• #### The PRL Mathematics Environment: A Knowledge Based Medium ﻿

(Cornell University, 1986-08)
ABSTRACT NOT SUPPLIED
• #### Proofs as Programs ﻿

(Cornell University, 1982-02)
The significant intellectual cost of programming is for problem solving and explaining and not for coding. Yet, programming systems offer mechanical assistance exclusively with the coding process. Here we describe an ...
• #### Writing Programs that Construct Proofs ﻿

(Cornell University, 1984-10)
When we learn mathematics, we learn more than definitions and theorems. We learn techniques of proof. In this paper, we describe a particular way to express these techniques and incorporate them into formal theories and ...