faculty.gif (20410 bytes)
choices.gif (4488 bytes)

Robert L. Constable

Professor and Chair
rc@cs.cornell.edu
http://www.cs.cornell.edu/home/rc/index.html

PhD Univ. of Wisconsin, Madison, 1968

I continue to work on type theory and automated reasoning, an inexhaustible source of fascinating problems in logic and computing theory. This year, K. Crary and I made further progress on the long-standing problem of constructively axiomatizing partial functions. Crary improved on and implemented a theory of "bar types" for use in the semantics of his object-oriented extension to ML. J. Hickey, Crary, S. Allen, and I have been comparing various notions of subtyping. In addition, E. Moran and I looked at some of the issues of defining P. Aczel's constructive set theory, CZF, in Nuprl and discovering ways to bring out the

 bob.tif (83588 bytes)
computational content of the very abstract results of this theory. My hope is to use CZF to explain D. Howe's new set-based semantics for Nuprl. Howe's results have opened a new chapter in automated reasoning by showing how to interpret HOL in classical Nuprl (a Nuprl subset without intersection and bar types to which P or not P is added).

I continue to explore ways to express computational complexity in type theory. The new bar types offer another avenue, which complement my results from 1994 on defining polynomial time logical operators. This work is supported by ONR.

The Nuprl group's major verification work now centers on Ensemble and is joint with K. Birman and his group, supported by DARPA. Our activity is centered on M. Hayden's OCaml implementation of Ensemble and on his technique for symbolically computing "fast track" paths through a protocol stack based on properties of the messages. Experiments show that fast tracking substantially improves performance. Hayden is working with C. Kreitz and J. Hickey to employ Nuprl in automatically reconfiguring the protocol stacks and proving that the reconfigured stack is equivalent to the original. Hickey and Hayden plan to combine Nuprl Light and Ensemble to enable Nuprl to run concurrently.

P. Naumov and I are working on a library of Nuprl lessons to be presented on the Web as supplemental material for courses on computational discrete mathematics, logic, automata theory, and programming language semantics. Allen and I are creating basic lessons on functions. Caldwell has a library on propositional calculus, and Naumov has libraries on the Simple Imperative Language (SIPL) from the CS611 textbook by C. Gunter, Semantics of Programming Languages. The NSF funds this effort.

University Activities

  • Chair: Department of Computer Science

  • Applied Math Policy Committee

  • Cognitive Studies Executive Committee

  • Digital Future Steering Committee

  • Engineering College Climate Committee

Professional Activities

  • TpHOL Program Committee

  • Advisory Council: Princeton University Computer Science Department

  • Chairman, Advisory Board: University of Chicago Computer Science Department

  • Editor: J. Logic and Computation; Formal Methods in System Design; J. Symbolic Computation

  • Director: NATO Summer School, Marktoberdorf, Germany

  • Elected Member: Association for Symbolic Logic Council

  • General Committee Member: LICS

Lectures

  • An open logical programming environment. DARPA PI Meeting, Seattle, Jun. 1998.

  • The emergence of formalized mathematics. American Math Society, Oct. 1997.

  • The impact of computer science on mathematics, from education to research. Colgate Univ. ScienceSeries, Sept. 1997.

  • Verifying Ensemble in Nuprl. Invited lecture, TpHOL Conference, Aug. 1997. Six lectures on the mathematics and mechanics of relating formal theories. Marktoberdorf Summer School, Aug. 1997.

Publications

  • Constructively formalizing automata. Proof, Language and Essays in Honour of Robin Milner, MIT Press, Cambridge. (1998) (with P. Jackson, P. Naumov and J. Uribe).

  • Formalizing decidability theorems about automata. Computational Logic, editors U. Berger and H. Schwichtenberg, NATO Advanced Study Institute, International Summer School, Marktoberdorf, Germany, July 29-August 6, 1997, Springer, 1998. The structure of Nuprl's type theory in logic and computation. NATO ASI Series, Schwichten_berg and Broy, eds., Springer-Verlag, (1997).

  • The structure of Nuprl's type theory in logic and computation. NATO ASI Series, Schwichten_berg and Broy, eds., Springer-Verlag, (1997).