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 MartinLof'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 problemsolving environments for mathematics and
engineering. Our current system is Nuprl 4, a 100,000line LispML
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 highlevel 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 problemsolving
methods. The system now ranks as one of the major tacticoriented
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 MartinLöf type theory. Celebrating 25 Years of
MartinLö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:

19951996 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).