Robert L. Constable

 Professor today

Department 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 Mathematics

1965  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. 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

Collaborators

AWARDS

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

RECENT PUBLICATIONS

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.

PUBLICATIONS MOST RELEVANT TO RESEARCH

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).

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.