**
The Triumph of Types: Principia Mathematica's Impact on Computer Science **

unofficial copies
[PDF]

by Robert L. Constable

Presented at the
*Principia Mathematica* anniversary symposium in 2010.

**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 influence 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 definitive 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.