Robert L. Constable
Professor and Chair
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
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.
- Chair: Computer Science Department
- Director: PRL Project
- Member: Cognitive Studies Executive Committee; Applied Math Policy
- 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
- 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,
- Type theory. Computer Science, Tel Aviv University, Israel, February,
- The value of automated deduction. NSF Workshop on the Future of
Automated Deduction, Chicago, March, 1995.
1995-1996 Annual Report Home Page
Departmental Home Page
If you have questions or comments please contact:
Last modified: 1 November 1996 by Denise Moore