Skip to main content
PRL Project

next up previous
Next: Keshav K. Pingali Up: Biographical Sketches Previous: L. Paul Chew

Robert L. Constable

 Professor today

Department of Computer Science `` (607) 255-9204 (office)

4149 Upson Hall (607) 273-5659 (home)

Cornell University

Ithaca, New York 14853 citizenship: United States


 1964  A.B., Princeton Mathematics

1965 M.A., University of Wisconsin Mathematics

1968 Ph.D., University of Wisconsin Mathematics


Professor, Department of Computer Science, Cornell University

Associate Professor, Department of Computer Science, Cornell University

Assistant Professor, Department of Computer Science, Cornell University

Instructor, University of Wisconsin


 1969 Allan B. Borodin  1980 Tat-Hung Chan 1987 
Douglas J. Howe

1970 Forbes D. Lewis 1981 Scott D. Johnson 1987 N. P. Mendler

1972 Robert V. Harris 1981 John P. Privitera 1988 Timothy G. Griffin

1972 John C. Cherniavsky 1982 Dean B. Krafft 1988 Scott F. Smith

1973 Stephen S. Muchnick 1985 Ryan D. Stansifer 1990 Chetan Murthy

1974 Kurt Mehlhorn 1985 Robert W. Harper 1990 David Basin

1976 Edmund M. Clarke, Jr. 1986 James T. Sasaki 1994 Paul Jackson

1976 Michael J. O'Donnell 1987 W. Rance Cleveland 1994 Wilfred Chen

1979 Joseph L. Bates 1987 Todd B. Knoblock 1994 Judith Underwood

1980 Carl Hauser 1987 Stuart F. Allen

Thesis Supervisor


ACM Fellow - 1994
John Simon Guggenheim Fellowship - 1990
Outstanding Educator Award - 1987


  1. Metalogical Frameworks. In Logical Environments, editors G. Huet and G. Plotkin, Chapter 1, pages 1-29, Cambridge University Press, 1993 (with D. Basin).

  2. Metalevel programming in constructive type theory. Programming and Mathematical Method, NATO ASI Series, Vol. F88, editor M. Broy, pages 45-93. Springer-Verlag, 1992.

  3. Implementing Metamathematics as an Approach to Automatic Theorem Proving. A Source book of Formal Techniques in A.I., pages 45-75. North-Holland, 1990 (with D. Howe).

  4. Finding Computational Content from Classical Proofs. Proceedings of the B.R.A Workshop on Logical Frameworks, Sophia-Antipolis, France, June 1990 (with C. Murthy).

  5. Assigning Meaning to Proofs: a semantic basis for problem solving environments. NATO ASI Series, Vol. F55, editor M. Broy, pages 63-91. Springer-Verlag, 1989.


  1. Computational foundations of basic recursive function theory. Theoretical Computer Science, 121, pages 89-112, Elsevier, 1993 (with S. F. Smith).

  2. Implementing Mathematics with the Nuprl proof development system, Prentice-Hall, Engelwood Cliffs, NJ, 1986 (with PRL Group).

  3. Proofs as Programs. Trans. on Program. Lang. and Syst., 7(1):113-136, January 1985.

  4. Introduction to the PL/CV2 Programming Logic, Lecture Notes in Computer Science, Vol. 135, Springer-Verlag, NY, 1982 (with S. Johnson and C. Eichenlaub).

  5. A Programming Logic, Winthrop, Mass., 1978 (with Michael O'Donnell).


I have been leading the applied logic group in computer science which is engaged in the building and study of computer systems to formalize mathematics in a feasible and useful way. Three such systems have been implemented since 1978. The most recent system, Nuprl, is a 100,000-line Lisp/ML program used to implement a constructive theory of types. Nuprl was designed by Joe Bates and myself and has been extended by Douglas Howe and Stuart Allen. Systems such as Nuprl are useful formalizations of mathematics because they can evaluate the computational content of theorems. In principle, Nuprl is both a formal system of mathematics and a programming language. We are studying ways to make the programming component efficient enough to allow Nuprl to be used for high-level programming as well as for verification. I have been involved in formalizing metamathematics in the system as a way to enhance theorem proving power.

For the past four years, I have been interested in reflecting the Nuprl logic in itself. S. Allen, D. Howe, W. Aitken, and I have designed a usable theory. We are now implementing a reflective version of the system based on this theory. More recently, C. Murthy and I have been studying the extraction of computational content from classical proofs using Nuprl. Murthy's thesis includes his extraction of computation content from Higman's lemma, a major result, and his discovery of a fundamental correspondence between classical proofs and computations.

next up previous
Next: Keshav K. Pingali Up: Biographical Sketches Previous: L. Paul Chew

nuprl project
Tue Nov 21 08:50:14 EST 1995