Faculty of Computing and Information Science >
Computing and Information Science >
Computing and Information Science Technical Reports >
Please use this identifier to cite or link to this item:
|Title: ||The Triumph of Types: Principia Mathematica's Impact on Computer Science|
|Authors: ||Constable, Robert|
|Issue Date: ||16-Jul-2011|
|Citation: ||Proceedings of 10th Annual Oregon Programming Languages Summer School|
|Abstract: ||Types now play an essential role in computer science; their ascent originates from Principia Mathematica. Type checking and type inference algorithms are used to prevent semantic errors in programs, and type theories are the native language of several major interactive theorem provers. Some of these trace key features back to Principia.
This lecture examines the in°uence of Principia Mathematica on modern type theories implemented in software systems known as interactive proof assistants. These proof assistants advance daily the goal for which Principia was designed: to provide a comprehensive formalization of mathematics. For instance, the de¯nitive formal proof of the Four Color Theorem was done in type theory. Type theory is considered seriously now more than ever as an adequate foundation for both classical and constructive mathematics as well as for computer science. Moreover, the seminal work in the history of formalized mathematics is the Automath project of N.G. de Bruijn whose formalism is type theory. In addition we explain how type theories have enabled the use of formalized mathematics as a practical programming language, a connection entirely unanticipated at the time of Principia Mathematica's creation.|
|Description: ||Video available as the last entry on the Oregon Programming Languages Summer School - curriculum page: http://www.cs.uoregon.edu/Research/summerschool/summer11/curriculum.html|
|Appears in Collections:||Computing and Information Science Technical Reports|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.