Now showing items 1-7 of 7

    • Constructive Automata Theory Implemented with the Nuprl Proof Development System 

      Kreitz, Christoph (Cornell University, 1986-09)
      The Nuprl proof development system was designed for the computer-assisted problem solving in mathematics and programming. In particular it can be used for the development of mathematical proofs and of programs which are ...
    • Dead Code Elimination Through Type Inference 

      Hafizogullari, Ozan; Kreitz, Christoph (Cornell University, 1998-04)
      We introduce a method to detect and eliminate dead code in typed functional programming languages. Our approach relies on a type system with simple subtypes for specifying dead code and a type inference algorithm for ...
    • 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 ...
    • Formal Reasoning about Communication Systems I: Embedding ML into TypeTheory. 

      Kreitz, Christoph (Cornell University, 1997-07)
      We present a semantically correct embedding of a subset of the Ocaml programming language into the type theory of NuPRL. The subset is that needed to build the Ensemble group communication system. We describe the essential ...
    • Formal Reasoning about Communication Systems II: Automated Fast-TrackReconfiguration 

      Kreitz, Christoph (Cornell University, 1998-09)
      We present formal techniques for improving the performance of group communication systems built with the Ensemble toolkit. For common sequences of operations we identify a fast-track through a stack 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 ...
    • The Horus and Ensemble Projects: Accomplishments and Limitations 

      Birman, Kenneth P.; Constable, Robert; Hayden, Mark; Hickey, Jason; Kreitz, Christoph; Van Renesse, Robbert; Rodeh, Ohad; Vogels, Werner (Cornell University, 1999-10)
      The Horus and Ensemble efforts culminated a multi-year Cornell research program in process group communication used for fault-tolerance, security and adaptation. Our intent was to understand the degree to which a single ...