Robert L. Constable

Robert L. Constable
Professor and Chair
rc@cs.cornell.edu
http://www.cs.cornell.edu/Info/Annual96/Faculty/rc.html
Ph.D. University of Wisconsin, Madison, 1968

My research program has two major goals. On the theoretical side, I want to help create a foundational theory of computing that is adequate to explain the major computational phenomena that determine how we shape "cyberspace". For many years, I have believed that a computational type theory is the right framework for this endeavor. Stuart Allen, Joseph Bates, and I have designed a theory in the tradition of Automath and Martin-Lof's type theories. These theories have generated a large literature and an energetic following. They are especially useful in programming language semantics. This year, I have tried to find natural ways to express computational complexity considerations in this context, with promising results.

My second major goal (pursued with students and colleagues) is the implementation of this foundational theory. The resulting systems have proven useful as problem-solving environments for mathematics and engineering. Our current system is Nuprl 4, a 100,000-line Lisp-ML hybrid. It is being used for circuit synthesis (by Miriam Leeser and her students), for programming language semantics (for Polya by Stuart Allen), for defining the types of a computer algebra system (for Weyl by Paul Jackson and Richard Zippel), and for accumulating a database of mathematical knowledge. Nuprl contains a very high-level lazy functional programming language. We are exploring the use of dependent types and subtypes in this language, and we are testing the notion that we can force software artifacts to be mathematical objects.

We also use Nuprl to explore ways of automating problem-solving methods. The system now ranks as one of the major tactic-oriented theorem provers because of the extensive work over the years of Doug Howe, David Basin, and Paul Jackson in building a large tactic library. The system supports a special formal hypertext mathematics editor designed by Stuart Allen, which makes it uncommonly effective in creating formal text. A number of dedicated users have contributed to the growing library of formalized constructive mathematics. I am using it with students to create formal metamathematics and fragments of automata and computability theory.

University Activities

Chair: Computer Science Department
Director: PRL Project
Member: Cognitive Studies Executive Committee; Applied Math Policy Committee

Professional Activities

Editor: Journal of Logic and Computation; Formal Methods in System Design; Journal of Symbolic Computation
Director: NATO Summer School, Marktoberdorf, Germany
Member: Association for Symbolic Logic Council; LICS General Committee

Lectures

Type theory as a foundation for computer science. Computer Science, Leeds University, England, October 1995.
Expressing computational complexity in type theory. Cambridge Newton Institute, Cambridge, England, October 1995.
Challenges for Martin-Löf type theory. Celebrating 25 Years of Martin-Löf Type Theory, Venice, Italy, October 1995.
Expressing computational complexity in type theory. Computer Science, Edinburgh, Scotland, September 1995.
Constructing and applying formal theories using the Nuprl mathematics environment. NATO Summer School, Marktoberdorf, Germany, July 1995.
Travels with Nuprl. Computer Science, Ben Gurion University, Israel, March 1996.
Type theory. Computer Science, Tel Aviv University, Israel, February, March 1996.

Publications

The value of automated deduction. NSF Workshop on the Future of Automated Deduction, Chicago, March, 1995.

Return to:

1995-1996 Annual Report Home Page
Departmental Home Page If you have questions or comments please contact: www@cs.cornell.edu. Last modified: 1 November 1996 by Denise Moore (denise@cs.cornell.edu).