Seminars

The Rise of Type Theory:  From Principia Mathematica to Constructive Type Theory, circa 1910-2010 (PDF)

Robert Constable
Cornell Univ., Computer Science Department

03/19/2012, 3:30 PM, GHC-3305

Abstract

We will explore a main line of type theory as it evolved from a foundation for mathematics, where it faltered, to a foundation for computer science, especially for programming language semantics and formal methods, where it has made steady progress. I will highlight particular ideas that have contributed to the success of computational type theory such as its grounding in a Turing complete polymorphic programming language with higher type functions, the central role of dependent types, recursive types, and co-recursive types, and the role of universes.

One sign of success is that constructive type theory is the native language of the interactive theorem provers  Agda, Coq, MetaPRL, Minlog, and Nuprl.  Classical type theory based on Church's simple type theory is the native language of the HOL family of provers. Among these provers, only MetaPRL and Nuprl are based on an extensional intuitionistic type theory.  I will point out the advantages and disadvantages of that choice and the important role of quotient types and subset types (refinement types).

The lecture will conclude with some thoughts on why intuitionistic type theory is a particularly appropriate foundation for distributed systems, one of the core topics of modern computer science. In that context, I will illustrate the role of a constructive version of the FLP theorem which I proved in 2008.

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 PhD 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 PhD supervisor at the University of Wisconsin was Stephen C. Kleene another such pioneer.