Building Reliable, High-Performance Networks
with the Nuprl Proof Development System


Christoph Kreitz.


Journal of Functional Programming 14(1):21-68, 2004.


Abstract

Proof systems for expressive type theories provide a foundation for the verification and synthesis of programs. But despite their successful application to numerous programming problems there remains an issue with scalability. Are proof environments capable of reasoning about large software systems? Can the support they offer be useful in practice?

In this article we answer this question by showing how the Nuprl proof development system and its rich type theory have contributed to the design of reliable, high-performance networks by synthesizing optimized code for application configurations of the Ensemble group communication toolkit.

We present a type-theoretical semantics of OCaml, the implementation language of Ensemble, and tools for automatically importing system code into the Nuprl system. We describe reasoning strategies for generating verifiably correct fast-path optimizations of application configurations that substantially reduce end-to-end latency in Ensemble. We also discuss briefly how to use Nuprl for checking configurations against specifications and for the design of reliable adaptive network protocols.


  (Preprint) BACK
Back to overview of papers


Bibtex Entry

@Article{ar:Kreitz04a, author = "Christoph Kreitz", title = "Building Reliable, High-Performance Networks with the {Nuprl} Proof Development System", journal = "Journal of Functional Programming", year = "2004" volume = 14, number = 1, pages = "21--68", }