theory. This is tricky because type theory is based on total computable functions while complexity
Robert L. Constable
Professor and Chair
PhD Univ. of Wisconsin, Madison, 1968
I continue to work on type theory, automated reasoning, and system verification — an inexhaustible source of fascinating
problems in computer science and logic
For several years, I have been trying to bring together two of the major theories in computer science,
computational complexity theory and type theory. The key step is to find
natural ways to express computational complexity
theory is based on algorithms and computations. Functions are more abstract than algorithms, e.g. two algorithms with different complexity properties are equal as functions if they compute the same result. One promising approach to expressing complexity arises by reflecting the term structure of type theory only enough to capture complexity properties, and using the notion of partial types developed with Karl Crary (building on earlier work that Scott Smith and I did) to capture the idea of an algorithm. The results are promising and have been well received at two
invited lectures this year.
The PRL group's major verification work centers on Ensemble and is joint with K. Birman, Robbert van Renesse and the Ensemble group, supported by
DARPA. This year Jason Hickey, Christoph Kreitz and Robbert have made substantial progress on using Nuprl to optimize protocol stacks. They have been able to automatically improve code in the Ensemble group communication system that manages fault-tolerant distributed computing. The improved code operates two to three times faster than the original and is generated in a matter of minutes
from the original. Comparable improvements done by hand took months of tedious and complex work on smaller examples, and the complexity led to errors in the faster code. In contrast, the automatic tools do not introduce errors. Nuprl shows that the improved code computes the same results as the original, so the code modifications are guaranteed to be correct.
In addition, Jason Hickey and Mark Bickford have created a Nuprl library that implements parts of a correctness proof for Ensemble Total Order that Jason, Robbert and Nancy Lynch wrote last year. This library will eventually enable a new component-based verification method that will apply to a wide variety of systems. Jason, Aleksey Nogin, and Alexie Kopylov are rebuilding this
capability in MetaPRL. Jason began the implementation of MetaPRL three years ago, and it is now running in a beta version that has attracted outside users and is being developed also in
Moscow. Jason and Aleksey have made MetaPRL one of the fastest theorem provers around. Its
implementation of the Nuprl type theory is a hundred times faster than Nuprl 4.
MetaPRL will become the backbone logic engine for our theorem proving work. It will be connected to Nuprl components to form our first Logical Programming Environment.
Stuart Allen, Pavel Naumov and I are working on a library of Nuprl lessons to be presented on the Web as supplemental material for courses on computational discrete mathematics, logic, automata theory, and programming language semantics. Allen is creating basic lessons on functions and counting. Caldwell has a library on propositional calculus, and Naumov has libraries on the Simple Imperative Language
(SIPL) from the CS611 textbook by C. Gunter, Semantics of
Programming Languages. The NSF funds this effort. The material has been used in Cornell courses.
Amanda Holland-Minkley, Regina Barzilay, Claire Cardie and I have started an effort to
automatically translate Nuprl proofs into English. Amanda and Regina have connected the FUF natural language generation system to Nuprl and discovered ways to extract the discourse knowledge and linguistic information that FUF
needs from the Nuprl proofs in the special
case of theorems in the basic number theory library. We are proposing to collaborate with the verification group at
Saarbucken, Germany who also work on proof translation.
Chair: Department of Computer Science
Applied Math Policy Committee
Cognitive Studies Executive Committee
Engineering College Climate Committee
Computing and Information Science Task Force
- Advisory Council: Princeton
Univ. Computer Science
- Chairman, Advisory Board:
Univ. of Chicago Computer Science Department
Chairman, Review Committee: Colgate Univ. Computer
Editor: Journal Logic and
Methods in System Design;
Director: NATO Summer
General Committee Member:
- Member: Computing and
Information Sciences Task Force
A Module Mechanism for Developing Algebra in Nuprl,
Invited Lecture, Calculemus and Types, Eindhoven, Netherlands, July
- Proof Technology circa 2000, Invited Lecture, CADE 15, Lindau,
Germany, July 1998
Expressing computational complexity in constructive type
theory. Invited talk. Implicit
Computational Complexity in
Programming Languages, Baltimore, Sept.. 1998
Listening to theorem provers
who talk to each other about
Distinguished lecture series, CMU, Oct 1998
A logical programming
environment suitable for building and managing modular systems.
DARPA Workshop, Stanford,
Verifying distributed systems
with a hybrid theorem prover.
Univ. of Wyoming, Leramie,
Wyoming, Nov 1998
Admiring proof reflections and working with them. Invited
lecture. Feferest, Stanford, Dec.
Applications of classes and types to verifying modular
systems. Invited talk. School of
Logic and Computation, Edinburgh, Apr. 1999
in an open logical programming
Workshop, Cornell Univ., May
Cornell in the information age.
Invited talk. Cornell Board of
Trustees, June 1998
- Types in logic, mathematics and
programming. In Handbook of Proof
Theory. (S. R. Russ,
ed.), Elsevier Science B.V.
- A note on complexity measures for inductive classes in
constructive type theory. In
Information and Computation
143 (1998), 137-153
Verbalization of high-level
formal proofs. In Proceedings
of the Sixteenth National
Conference on Artificial
Intelligence AAAI (July 1999)
(with A. Holland-Minkley and