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 longstanding problem of constructively
axiomatizing partial functions. Crary improved on and implemented a theory of "bar
types" for use in the semantics of his objectoriented 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 

computational content of the very abstract
results of this theory. My hope is to use CZF to explain D. Howe's new setbased 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 29August 6, 1997, Springer,
1998. The structure of Nuprl's type theory in logic and computation. NATO ASI Series,
Schwichten_berg and Broy, eds., SpringerVerlag, (1997).
The structure of Nuprl's type theory in logic and
computation. NATO ASI Series, Schwichten_berg and Broy, eds., SpringerVerlag,
(1997).
