Colloquium Details
Distinguished Lecture Series: What is a Proof? — Some Challenges for Automated Theorem Proving
| Author: | Dana Scott Carnegie Mellon University |
|---|---|
| Date: | June 22, 2011 |
| Time: | 19:00 |
| Location: | 110 Knight Law Center |
| Host: | Zena Ariola |
Abstract
One popular notion of a (Scott-Ersov) domain is defined as a bounded complete algebraic cpo. Such an abstract a definition is not always so helpful for beginners. The speaker found recently that there is an easy-to-construct domain of countable semilattices giving isomorphic copies of all countably based domains. This approach seems to have advantages over both the so-called "information systems" and the more abstract lattice/ topological definitions, and it makes the finding of solutions to domain equations and models for the lambda-calculus very elementary to justify. The "domain of domains" also has a natural computable structure in this formulation. Built on top of this construction is a modeling of Martin-Löf type theory.
This talk is given as part of the Oregon Programming Languages Summer School. The complete schedule is available.
Biography
Dana Scott, a native of California, received his B.A. in Mathematics at U.C. Berkeley in 1954, and his Ph.D. in Mathematics at Princeton in 1958. He has been awarded honorary degrees at Utrecht, Darmstadt, Edinburgh, and Ljubljana. He has taught at the University of Chicago, U.C. Berkeley, Stanford, Amsterdam, Princeton, Oxford (U.K.), Carnegie Mellon, and Linz (Austria). He became Professor Emeritus in July of 2003.
He has been a Bell Telephone Fellow, Miller Institute Fellow, Alfred P. Sloan Research Fellow, Guggenheim Foundation Fellow, Visiting Scientist at Xerox PARC, Visiting Professor at the Institut Mittag-Leffler, Sweden, and most recently a Humbolt Stiftung Senior Visiting Scientist, Munich, Germany. He is a fellow of the Academia Europaea, American Association for the Advancement of Science, American Academy of Arts and Sciences, Association for Computing Machinery, British Academy, Finnish Academy of Sciences and Letters, New York Academy of Sciences, and U.S. National Academy of Sciences.
He received the LeRoy P. Steele Prize of the American Mathematical Society, the Turing Award (with Michael Rabin) of the Association for Computing Machinery, the Harold Pender Award, University of Pennsylvania, the Rolf Schock Prize in Logic and Philosophy, Royal Swedish Academy of Sciences, the Bolzano Medal for Merit in the Mathematical Sciences of the Czech Academy of Sciences, and the Gold Medal of the The Sobolev Institute of Mathematics, Novosibirsk, Russia.
Over the years he has been supervisor of forty-two Ph.D. students.