Two students walking on Engineering Quad towards Duffield
Woman taking a photo of a mumified bird
Duffield Hall at sunset.
Two students working on a autonomous plane
Students walking along Ho Plaza

Robert Constable

Professor
Computer Science

Biography

Robert L. Constable heads the PRL research group in automated reasoning and formal methods. Starting in 1983 and continuing to this day, he and by now over forty collaborators, have built, used and extended the Nuprl interactive theorem prover and the Logical Programming Environment it supports. Currently Nuprl is used in creating correct-by-construction distributed protocols. Nuprl’s implementation since 2000 is itself a distributed system.

Professor Constable joined the Cornell Computer Science Department in 1968.

He has supervised over forty Ph.D. students in computer science. He is known for designing and implementing formal theories of constructive mathematics that also serve as programming languages, a plan he outlined in 1971. This work has led to new ways of automating the production of reliable software.

He has written three books on this topic as well as numerous research articles in computing theory, type theory, programming languages, and formal methods. Professor Constable was an undergraduate at Princeton University where he worked with Alonzo Church, one of the pioneers of type theory and the theory of computing.

His Ph.D. supervisor at the University of Wisconsin was Stephen C. Kleene another such pioneer.

Research Interests

My research is on computer assisted reasoning, correct software development, formal methods, applied logic, the formal semantics of programming languages, type theory, and the design of logical programming environments.

Teaching Interests

I teach formal methods and programming languages and have in the past taught Theory B, semantics.

Selected Publications

  • Constable, Robert Lee, Mark Bickford, Vincent Rahli. 2016.“A Story of Bar Induction in Nuprl”.
  • Constable, Robert Lee, L. Cohen. 2015.“Intuitionistic Ancestral Logic.”Journal of Logic and Computation.
  • Bickford, Mark, Robert Lee Constable, Richard Eaton, Vincent Rahli. 2015.“Nuprl’s Inductive Logical Forms”Paper presented at AI4FM, Edinburgh, UK, September.
  • Rahli, Vincent, David Guaspari, Mark Bickford, Robert Lee Constable. 2015.“Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML.”Proceedings of the 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015)
  • Bickford, Mark, Robert Lee Constable. 2013.“Polymorphic Logic.”In Logic, Construction, Computation, edited by Ulrich Berger, Hannes Diener, Peter Schuster, Monika Seisenberger, 51-66. Ontos Verlag.

Selected Awards and Honors

  • Herbrand Award2014
  • ACM Fellow(ACM)1994
  • John Simon Guggenheim Fellowship1990
  • Outstanding Educator Award(Cornell University)1987

Education

  • A.B.(Mathematics), University of Wisconsin, 1964
  • M.A. (Mathematics), University of Wisconsin, 1965
  • Ph.D. (Mathematics), University of Wisconsin, 1968

Websites