**Next:**Keshav K. Pingali

**Up:**Biographical Sketches

**Previous:**L. Paul Chew

## Robert L. Constable

Professor todayDepartment of Computer Science `` (607) 255-9204 (office)

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

Cornell University rc@cs.cornell.edu

Ithaca, New York 14853 citizenship: United States

** EDUCATION**

1964 A.B., Princeton Mathematics1965 M.A., University of Wisconsin Mathematics

1968 Ph.D., University of Wisconsin Mathematics

** ACADEMIC POSITIONS**

- 1978-
- Professor, Department of Computer Science, Cornell University
- 1972-78
- Associate Professor, Department of Computer Science, Cornell University
- 1968-72
- Assistant Professor, Department of Computer Science, Cornell University
- 1968-68
- Instructor, University of Wisconsin

** PH. D. STUDENTS ADVISED**

1969 Allan B. Borodin 1980 Tat-Hung Chan 1987 Douglas J. Howe1970 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**

##### **
Collaborators**

** AWARDS**

ACM Fellow - 1994

John Simon Guggenheim Fellowship - 1990

Outstanding Educator Award - 1987

** RECENT PUBLICATIONS**

- Metalogical Frameworks. In
*Logical Environments*, editors G. Huet and G. Plotkin, Chapter 1, pages 1-29, Cambridge University Press, 1993 (with D. Basin). - Metalevel programming in constructive type theory.
*Programming and Mathematical Method*, NATO ASI Series, Vol. F88, editor M. Broy, pages 45-93. Springer-Verlag, 1992. - 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). - Finding Computational Content from Classical Proofs.
*Proceedings of the B.R.A Workshop on Logical Frameworks*, Sophia-Antipolis, France, June 1990 (with C. Murthy). - 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.

** PUBLICATIONS MOST RELEVANT TO RESEARCH**

- Computational foundations of basic recursive function theory.
*Theoretical Computer Science*, 121, pages 89-112, Elsevier, 1993 (with S. F. Smith). -
*Implementing Mathematics with the Nuprl proof development system*, Prentice-Hall, Engelwood Cliffs, NJ, 1986 (with PRL Group). - Proofs as Programs.
*Trans. on Program. Lang. and Syst.*, 7(1):113-136, January 1985. -
*Introduction to the PL/CV2 Programming Logic*, Lecture Notes in Computer Science, Vol. 135, Springer-Verlag, NY, 1982 (with S. Johnson and C. Eichenlaub). -
*A Programming Logic*, Winthrop, Mass., 1978 (with Michael O'Donnell).

** RESEARCH ACCOMPLISHMENTS**

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:**Keshav K. Pingali

**Up:**Biographical Sketches

**Previous:**L. Paul Chew

*nuprl project*

Tue Nov 21 08:50:14 EST 1995

Tue Nov 21 08:50:14 EST 1995