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.

University Activities

Dean: Computing and Information Science.

Committees: Applied Math Policy; Cognitive Studies Executive Committee.

Professional Activities

Advisory Council: Princeton University Computer Science Department.

Chairman, Advisory Board: University of Chicago Computer Science Department.

Editor: Journal Logic and Computation; Formal Methods in System Design; Journal of Symbolic Computation.

Director: NATO Summer School, Marktoberdorf, Germany.

General Committee Member: LICS.

Lectures

Reasoning about Automata and Protocols in Constructive Type Theory. Marktoberdorf, 4 lectures, August 1999.

Academic Computer Science in the Information Age. Cornell University Dept. of Computer Science Colloquium, Ithaca, NY, September 1999.

The Role of Verification in Tolerant Networking. DARPA PI meeting, Rome, NY, October 1999.

Progress in Achieving Interoperability of Formal Tools. DARPA PI meeting, Arlington, VA, October 1999.

Formal Methods for Software Evolution: Interoperability Results. Arlington, VA, October 1999.

Academic CS and the Information Age. CS Dept. Colloquium, University of Rochester, Rochester, NY, November 1999.

—. CS Dept. Colloquium, University of Buffalo, Buffalo, NY, November 1999. Universities in the Information Age. CS Dept. Colloquium, Ben Gurion Univ., Israel, January 2000.

—. Computing Continuum Conference, San Francisco, CA, March 2000. Computer Science: Achievements and Challenges. Ben Gurion University, Israel, March 2000.

Progress in Designing, Building and Testing Open Logical Programming Environments. DARPA PI meeting, Portland, OR, March 2000.

Lectures in Types in Logic, Mathematics and Programming. EEF Foundations School, 3 lectures, Edinburgh, Scotland, April 2000.

Formal Support for High Confidence Software Systems. Washington, DC, April 2000.

Developing Reliable Software Using a Logical Programming Environment. Rome, NY, June 2000.

Publications

“Building Reliable, High-Performance Communication Systems from Components.” In Proc. of the 17th ACM Symposium on Operating System Principles, Kiawah Island Resort, SC (December 1999), 80–92 (with X. Liu, C. Kreitz, R. van Renesse, J. Hickey, M. Hayden, and K. Birman).

“The Horus and Ensemble Projects Accomplishments and Limitations.” In DISCEX ’00, Hilton Head, SC (January 2000), Vol. I (October 1999), 149–161 (with K. Birman, R. van Renesse, O. Rodeh, and W. Vogels).

“Constructively Formalizing Automata.” In Proof, Language and Interaction: Essays in Honour of Robin Milner, MIT Press, Cambridge (2000), 213–238 (with P.B. Jackson, P. Naumov, and J. Uribe).

“Nuprl’s Class Theory and its Applications.” In Foundations of Secure Computation, F.L. Bauer and R. Steinbruggen (Eds.) IOS Press, (2000), 91–115.

“The Nuprl open logical environment.” In 17th International Conference on automated deduction, volume 1831 of Lecture Notes in Artificial Intelligence. Springer Verlag, 2000 (with S. Allen, R. Eaton, C. Kreitz, and L. Lorigo).