Now showing items 1-2 of 2

    • Concurrent Refinement in Nuprl 

      Moten, Roderick (Cornell University, 1997-08)
      This dissertation reports on the design, implementation, and analysis of the first parallel interactive theorem prover, called the MP refiner. The MP refiner is a shared memory multi-processor implementation of the inference ...
    • Nuprl as a Generic Theorem Prover 

      Moten, Roderick (Cornell University, 1996-04)
      Logical Frameworks are one way to provide generic theorem provers. This paper describes another method using loose semantics. In the paper, we explain loose semantics, describes its use in building a programming calculus ...