Now showing items 7-12 of 12

    • 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. ...
    • 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 ...
    • Transforming the Academy: Knowledge Formation in the Age of Digital Information 

      Constable, Robert (Cornell University, 2005-02-08)
      Computer-mediated knowledge formation will profoundly change every academic discipline and pose fundamental challenges to the mission of the modern research university in teaching the new knowledge, securing sound methods ...
    • The Triumph of Types: Principia Mathematica's Impact on Computer Science 

      Constable, Robert (2011-07-16)
      Types now play an essential role in computer science; their ascent originates from Principia Mathematica. Type checking and type inference algorithms are used to prevent semantic errors in programs, and type theories are ...