Now showing items 1-10 of 10

    • A Causal Logic of Events in Formalized Computational Type Theory 

      Bickford, Mark; Constable, Robert L. (Cornell University, 2005-12-13)
      We provide a logic for distributed computing that has the explanatory and technical power of constructive logics of computation. Inparticular, we establish a proof technology that supports correct-by-construction programming ...
    • FDL: A Prototype Formal Digital Library 

      Allen, Stuart; Bickford, Mark; Constable, Robert; Eaton, Richard; Kreitz, Christoph; Lorigo, Lor (Cornell University, 2004-06-16)
      This manual describes the first prototype of a new kind of system which we call a Formal Digital Library (FDL). We designed the system and assembled the prototype as part of a research project sponsored by the Office of ...
    • Formally Verifying Hybrid Protocols with the Nuprl Logical ProgrammingEnvironment 

      Bickford, Mark; Kreitz, Christoph; van Renesse, Robbert (Cornell University, 2001-05-09)
      We describe a generic switching protocol for the construction of hybrid protocols and prove it correct with the Nuprl proof development system. We introduce the concept of meta-properties to characterize communication ...
    • 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 ...