Now showing items 8-10 of 10

    • A Logic of Events 

      Bickford, Mark; Constable, Robert L. (Cornell University, 2003-03-07)
      There is a well-established theory and practice for creating correct-by-construction functional programs by extracting them from constructive proofs of assertions of the form "For all x:A there exists y:B.R(x,y))." There ...
    • The Logic of Events, a framework to reason about distributed systems 

      Bickford, Mark; Constable, Robert; Rahli, Vincent (2012 Languages for Distributed Algorithms (LADA) workshop, 2012-01-23)
    • A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics. 

      Allen, Stuart F.; Bickford, Mark; Constable, Robert; Eaton, Richard; Kreitz, Christoph. (Cornell University, 2003-02-03)
      We describe a link between the Nuprl and PVS proof systems that enables users to access PVS from the Nuprl theorem proving environment, to import PVS theories into the Nuprl library, and to browse both Nuprl and PVS ...