Now showing items 10-12 of 12

    • 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 ...