Robert L. Constable
Professor and Chair
rc@cs.cornell.edu
http://www.cs.cornell.edu/home/rc/DefaultRC.htm
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
in type 

theory. This is tricky because type theory is based on total computable functions while 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 faulttolerant 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 componentbased 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 HollandMinkley, 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.
University Activities

Chair: Department of Computer Science

Applied Math Policy Committee

Cognitive Studies Executive Committee

Engineering College Climate Committee

Computing and Information Science Task Force Professional Activities
 Advisory Council: Princeton
Univ. Computer Science
Department
 Chairman, Advisory Board:
Univ. of Chicago Computer Science Department

Chairman, Review Committee: Colgate Univ. Computer
Science Dept.

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

Director: NATO Summer
School, Marktoberdorf,
Germany

General Committee Member:
LICS
 Member: Computing and
Information Sciences Task Force
Lectures

A Module Mechanism for Developing Algebra in Nuprl,
Invited Lecture, Calculemus and Types, Eindhoven, Netherlands, July
1998.
 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
computer systems.
Distinguished lecture series, CMU, Oct 1998

A logical programming
environment suitable for building and managing modular systems.
DARPA Workshop, Stanford,
Oct 1998

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.
1998

Applications of classes and types to verifying modular
systems. Invited talk. School of
Logic and Computation, Edinburgh, Apr. 1999

Componentbased verification
in an open logical programming
environment. DARPA
Workshop, Cornell Univ., May
1998

Cornell in the information age.
Invited talk. Cornell Board of
Trustees, June 1998
Publications
 Types in logic, mathematics and
programming. In Handbook of Proof
Theory. (S. R. Russ,
ed.), Elsevier Science B.V.
(1998), 683786
 A note on complexity measures for inductive classes in
constructive type theory. In
Information and Computation
143 (1998), 137153

Verbalization of highlevel
formal proofs. In Proceedings
of the Sixteenth National
Conference on Artificial
Intelligence AAAI (July 1999)
(with A. HollandMinkley and
R. Barzilay)
