1998 - 1999 CS Annual Report                                                                  Faculty
choices.gif (4488 bytes)

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

 bob.tif (83588 bytes)
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 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. 

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  
  • Component-based 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), 683-786 
  • 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
    R. Barzilay)