Skip to main content

Dependent Type Theories

Posted in
Vladimir Voevodsky
Mit, 2016-02-10 10:00 - 11:00
MPIM Lecture Hall

Modern dependent type theories exist mostly in the form of computer programs. As such they are objects of the physical reality more than they are objects of the mathematical one. For three decades the world of type theories was relatively calm - innovation was largely occurring in the layers of programming above the type theories leading to proof assistants with more and more sophisticated systems for notation, implicit arguments and tactics.

The discovery of the univalent models led to the addition of new features to the existing type theories as well as to the development of entirely new ones such as cubicaltt. Eventually, these new type theories will become the cores of proof assistants with much more convenient than before environments for formal verification of mathematical arguments.

It is clear that the only way to ensure that these new proof assistants are reliable - that any proof of “false” in such a proof assistant can be mechanically transformed into a proof of “false” in one of the “consistency standards”, is to have a system where a new proof assistant has to be formally certified using an already certified proof assistant against an already certified formal system before it can become accepted as a reliable tool in pure mathematics.

The strongest consistency standard available in pure mathematics is ZFC. This means that as a prerequisite  for such a certification system we need to have a mathematical theory of dependent type theories that can be formalized in ZFC. At the moment only fragments of this future theory exist. I will give an introduction to my vision of the theory by describing these fragments and pointing out the gaps.

Slides of the lectures can be found on my home page.

Datei Lecture_1.pdf112.58 KB
Datei Lecture_2.pdf136.13 KB
Datei Lecture_3.pdf128.54 KB
Datei Lecture_4.pdf128.89 KB
Datei Lecture_5.pdf128.12 KB
© MPI f. Mathematik, Bonn Impressum & Datenschutz
-A A +A