Robert L. Constable
Department Chair/Professor
rc@cs.cornell.edu

Ph.D. University of Wisconsin, Madison, 1968

Research

We are engaged in the study of computer systems that provide mechanical assistance in problem solving, especially in programming and mathematics. This involves a long term study of ways to make the formalization of mathematics feasible and useful. We have implemented three such systems in the past tne years: PL/CV, PRL, and Nuprl.

Our major experimentation is with Nuprl, a 60,000-line Lisp program that implements a constructive theory of types. Systems such as Nuprl are useful formalizations of mathematics because they can express a wide variety of proof and program-building methods as metalevel programs of the system. These provide considerable theorem proving power. Moreover, Nuprl is especially useful because it can evaluate the computational content of theorems. In principle, Nuprl is both a fomal system of mathematics and a programming language.

We continue to improve Nuprl; the current version used at Cornell is called Nuprl 4. It differs from its predecessors in having a new term editor designed by Stuart Allen and implemented by Richard Eaton. Its internal structure is more modular, making the system suitable for he definition of a wide variety of logics beyond the built-in constructive type theory. Also, the entire theorem-proving mechanism has been rebuilt and stream-lined by Paul Jackson, building on the work of Douglas Howe. This contributes to the generic nature of Nuprl 4. Finally, this version of the system can refer to itself. There is an internal description of the language and its logic built principally by William Aitken using the theory developed by Allen, Howe, and myself. Richard Eaton designed a link between the internal description of the logic and the logic itself, which makes it possible to prove theorems about the process of proving theorems.

We are also engaged in three exciting joint ventures. One is with Miriam Leeser of Electrical ENgineering and the other two are in Computer Science; with David Gries on Polya and with Richard Zippel on Weyl. With Lesser, we are involved in hardware synthesis and verification. Leeser and her student Mark Aagard have used Nuprl to prove the correctness of a 1000-line boolean circuit minimization package, Pbs, used by circuit designers. This is a component of Leeser's Bedroc system (it implements the weak division algorithm, which is widely used in circuit design systems). This major theorem proving effort taught us a great deal about the effectiveness of our technology in the hands of expert users from an application domain.

The second joint venture involves building a model of the Polya programming language and a program refinement mechanism for it, both designed by David Gries, which will enable him to write his handbook of algorithms in the manner that he devised through years of study of the programming process. Stuart Allen has givne a formal type-theoretic definition of Polya. We expect to be experimenting soon with transforms and trying to capture the programming style that Gries wants.

We have recently begun a collaboration that we hope to relate to the Polya effort. Conal Mannion has been exploring the possibility of using Nuprl in computational science. We have been discussing problems with Richard Zippel and are hoping to connect Zippel's symbolic algebra system, Weyl, with Nuprl in the near future. This will be used to explore the development of scientific computing software using Weyl and Nuprl together with other tools that Zippel is building.

Professional Activities

Editor, Journal of Symbolic Computation
Editor, Academic Press
Editor, Journal of Logic and Computation
Editor, Oxford University Press
General Chair, LICS
Program Committee, North American Jumelage
Program Committee, Theoretical Aspects of Computer Software
Referee/Reviewer: NSERC (Canada), NSF, Theoretical Computer Science

University Activities

Chair, Computer Science Recruiting Committee
Computer Science Computing Facilities Committee
Provost's Study Committee on Mathematics

Lectures

Formal theories and software systems: fundamental connections between
computer science and logic. INRIA's 25th Anniversary Celebration, Paris, France, December 1992.
The Nuprl software development system. Computer Science Colloquium, Ben
Gurion University, Ber Sheva, Israel, January 1993.
Formal theories and software systems. State of Israel Symposium, Tel Aviv,
Israel, January 1993.
___. Association for Symbolic Logic, Annual Meeting, Notre Dame University,
Notre Dame, Indiana, March 1993.
Metaprogramming in type theory. State University of New York, Buffalo,
New York, March 1993.
Formal explanations of software. Formal Methods and Software Engineering
Workshop, University of Pennsylvania, Philadelphia, Pennsylvania, May 1993.

Publications

Formal theories and software systems: fundamental connections between
computer science and logic. In Future Tendencies in Computer Science, Control and Applied Mathematics (ed. A Bensoussan and J.-P. Verjus) Lecture Notes in Computer Science 653, Springer-Verlag (December 1992), 105-127.
Metalevel programming in constructive type theory. In Programming and
Mathematical Method (ed. Manfred Broy), NATO ASI Series F88, Springer-Verlag (1992), 45-93.