Now showing items 4-10 of 10

    • Generating event logics with higher-order processes as realizers 

      Bickford, Mark; Constable, Robert; Guaspari, David (2011-08-25)
      Our topic is broadening a practical ”proofs-as-programs” method of program development to “proofs-as-processes”. We extend our previous results that implement proofs-as-processes for the standard model of asynchronous ...
    • Intuitionistic Completeness of First-Order Logic 

      Constable, Robert; Bickford, Mark (2011-10-07)
      We establish completeness for intuitionistic first-order logic, iFOL, showing that is a formula is provable if and only if it is uniformly valid under the Brouwer Heyting Kolmogorov (BHK) semantics, the intended semantics ...
    • Investigating correct-by-construction attack-tolerant systems 

      Constable, Robert; Bickford, Mark; Van Renesse, Robbert (2011-09-12)
      Attack-tolerant distributed systems change their protocols on-the-fly in response to apparent attacks from the environment; they substitute functionally equivalent versions possibly more resistant to detected threats. ...
    • Knowledge-Based Sythesis of Distributed Systems Using Event Structures 

      Bickford, Mark; Constable, Robert C.; Halpern, Joseph Y.; Petride, Sabina (Cornell University, 2004-02-13)
      To produce a program guaranteed to satisfy a given specification one can synthesize it from a formal constructive proof that a computation satisfying that specification exists. This process is particularly effective if ...
    • 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 ...