Now showing items 1-6 of 6

    • The Definition of $\mu$PRL 

      Bates, Joseph L.; Constable, Robert L. (Cornell University, 1982-10)
    • A Logic for Correct Program Development 

      Bates, Joseph L. (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 

      Constable, Robert L.; Bates, Joseph L. (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 

      Bates, Joseph L. (Cornell University, 1986-08)
    • Proofs as Programs 

      Bates, Joseph L.; Constable, Robert L. (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 

      Constable, Robert L.; Knoblock, Todd B.; Bates, Joseph L. (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 ...