JavaScript is disabled for your browser. Some features of this site may not work without it.
Browsing by Author "Bickford, Mark"
Now showing items 110 of 10

A Causal Logic of Events in Formalized Computational Type Theory
Bickford, Mark; Constable, Robert L. (Cornell University, 20051213)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 correctbyconstruction programming ... 
FDL: A Prototype Formal Digital Library
Allen, Stuart; Bickford, Mark; Constable, Robert; Eaton, Richard; Kreitz, Christoph; Lorigo, Lor (Cornell University, 20040616)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, 20010509)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 metaproperties to characterize communication ... 
Generating event logics with higherorder processes as realizers
Bickford, Mark; Constable, Robert; Guaspari, David (20110825)Our topic is broadening a practical ”proofsasprograms” method of program development to “proofsasprocesses”. We extend our previous results that implement proofsasprocesses for the standard model of asynchronous ... 
Intuitionistic Completeness of FirstOrder Logic
Constable, Robert; Bickford, Mark (20111007)We establish completeness for intuitionistic firstorder 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 correctbyconstruction attacktolerant systems
Constable, Robert; Bickford, Mark; Van Renesse, Robbert (20110912)Attacktolerant distributed systems change their protocols onthefly in response to apparent attacks from the environment; they substitute functionally equivalent versions possibly more resistant to detected threats. ... 
KnowledgeBased Sythesis of Distributed Systems Using Event Structures
Bickford, Mark; Constable, Robert C.; Halpern, Joseph Y.; Petride, Sabina (Cornell University, 20040213)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, 20030307)There is a wellestablished theory and practice for creating correctbyconstruction 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, 20120123) 
A NuprlPVS Connection: Integrating Libraries of Formal Mathematics.
Allen, Stuart F.; Bickford, Mark; Constable, Robert; Eaton, Richard; Kreitz, Christoph. (Cornell University, 20030203)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 ...