My research program has two major goals. On the theoretical side, I want to help create a foundational theory of computing 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 such an endeavor. Stuart Allen, Joseph Bates, and I have designed a theory in the tradition of Automath and Martin-Löf'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 hybrid of Lisp and ML. 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.
If you have questions or comments please contact: www@cs.cornell.edu.