Dean for Computing and Information Science
Ph.D. University of Wisconsin-Madison, 1968
I direct the PRL research group. For the past three years we have been building a system that we call a logical programming environment (LPE). It provides substantial automation in the design, coding, verification, and evolution of large software systems. Generally an LPE
will integrate programming languages and logics. In our case we integrate the ML programming language and a programming logic based on type theory. Reasoning about ML programs is founded on a type theoretic semantics for ML. The LPE also integrates a compiler and a theorem prover. We use the latest version of Nuprl, version 5, as the prover.
Over the past year we have deployed our prototype LPE to support the Ensemble group communication system that Ken Birman, Robbert van Renesse, and their students have built and are now using and improving. The LPE provides automatic code transformations that improve performance in a way that is guaranteed not to introduce errors. The LPE also supports the design and coding of new adaptive protocols that are part of the Spinglass project.
We follow the work of Greg Morrisett and his students on new ML compilers and on typed assembly language. We plan to use the LPE to broadly support research on language-based security in the department and at the new Information Assurance Institute, including the work of Dexter Kozen, Andrew Myers, and Fred Schneider.
The Nuprl 5 system is a major re-implementation of Nuprl 4; its design is based on communicating processes that synchronize around a logical database that we call “the Library.” The Library stores definitions, theorems, conjectures, proofs, proof tactics, and commentary that is linked to the formal mathematics. We are releasing a first version of Nuprl 5 this summer, with a debut at CADE in June involving the whole design and implementation team (Stuart Allen, Rich Eaton, Christoph Kreitz, Lori Lorigo, and I). Nuprl 5 supports multiple proof engines and multiple editors. It also integrates an automatic theorem prover, called the JProver, built by C. Kreitz, Jens Otten, and Stephan Schmitt.
We are also working on a more experimental LPE called MetaPRL, which started with Jason Hickey’s thesis and now involves many people but especially Aleksey Nogin and Alexsey Kopylov. This system is built entirely in OCaml and supports OCaml as its programming language. It is coded for efficiency as well as modularity and at some tasks is over two orders of magnitude faster than Nuprl 5. It also supports multiple programming logics. Nuprl 5 and Meta PRL can share mathematics libraries.
The two theorem provers are used in a variety of other projects as well, including the creation of formal courseware by S. Allen, the translation of formal proofs into natural language by Amanda Holland-Minkley, the automatic analysis of the computational complexity of higher-order programs by Ralph Benzinger, and efficient reflection being designed and implemented by Eli Barzilay.
Dean: Computing and Information
Chairman, Advisory Board: University
of Chicago Computer Science Department.