The Role of Type Theory: Principia Mathematica's Impact on Computer Science

Robert Constable

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.

Computational Type theory works well as a foundation for computer
science, and it is considered seriously now more than ever as an
adequate foundation for constructive mathematics. Possibly in due
course the classical version of CTT will be considered as an adequate
foundation for formalized classical mathematics. Notable in this
regard is that the seminal work in the history of formalized
mathematics is the Automath project of N.G. de Bruijn whose formalism
is classical type theory.

In addition, I will 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. In this context, I will present a short new
proof of Godel's first incompleteness theorem using a logic for
computable functions (LCF) formalized in type theory.