Show simple item record

dc.contributor.authorConstable, Robert
dc.identifier.citationProceedings of 10th Annual Oregon Programming Languages Summer Schoolen_US
dc.descriptionVideo available as the last entry on the Oregon Programming Languages Summer School - curriculum page:
dc.description.abstractTypes 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.en_US
dc.titleThe Triumph of Types: Principia Mathematica's Impact on Computer Scienceen_US
dc.typetechnical reporten_US

Files in this item


This item appears in the following Collection(s)

Show simple item record