Colloquium Details
Distinguished Lecture Series: Design Issues for Implemented Type Theories
| Author: | Robert Constable Cornell University |
|---|---|
| Date: | June 29, 2011 |
| Time: | 19:00 |
| Location: | 110 Knight Law Center |
| Host: | Zena Ariola |
Abstract
Significant theoretical differences among the major implemented type theories are based on design goals informed by metamathematical theorems and the results in the semantic theory of programming languages. These goals and design decisions are not often compared and analyzed in the literature. I will undertake such comparisons in this lecture, focusing on differences between Computational Type Theory (CTT), implemented in Nuprl and MetaPrl, and the Calculus of Inductive Constructions (CIC) implemented in Coq. Both theories are constructive and both use the LCF tactic mechanism for automation, but initial differences in goals have led to interesting practical consequences, some unexpected.
This talk is given as part of the Oregon Programming Languages Summer School. The complete schedule is available at www.cs.uoregon.edu/Activities/summerschool/summer11/schedule.html.
Biography
Professor Robert Constable is a graduate of Princeton University where he worked with Alonzo Church, one of the pioneers of computer science. He did his PhD at Wisconsin with Stephen Cole Kleene, a PhD student of Church and another pioneer of computer science. Church traces his mathematical lineage back to Gottfried Wilhelm Leibniz, one of the first logicians interested in mechanical computation and the digitization of human knowledge.
Professor Constable joined the Cornell faculty in 1968. He has supervised over forty Ph.D. students in computer science. He is known for his work connecting programs and mathematical proofs which has led to new ways of automating the production of reliable software. This work is known by the slogan "proofs as programs," and it is embodied in the Nuprl ("new pearl") theorem prover and Logical Programming Environment. He has written three books on this topic as well as numerous research articles.
Since 1980 he has headed a project that uses Nuprl to build software systems that are correct by construction, some instances of which are still operational in industry and science. Currently he is working on extending this programming method to concurrent processes, realizing the notion of "proofs as processes" and showing how to build attack tolerant systems.