Computational Type Theory


"A sufficiently expressive programming language is the foundations for all of mathematics" - Robert Harper OPLSS 2018

The goal is to understand the recent developments in computational type theory which came from Per Marin-Lof's intuitionistic type theory, and Vladimir Voevodsky's univalent foundations. Voedvodsky's plan was to create a new foundation for 'all of mathematics', create new proof assistants so mathematicians without pedigree can contribute to global mathematics research since their proofs can easily be verified, that AI can extend a model (itself) and generate it's own proofs for that model, and that math will in the future be done entirely in a programming language because the theory of programming languages he claims is the same thing as mathematical logic, they express the same ideas in a different language, so why not unify them.


You should google and read everything you can about Field's medalist Voevodsky and his work at the Institute of Advanced Studies at Princeton. He has many talks on YouTube well worth viewing, too many to list here but we'll watch some later in the workshop.

Here is the quick rundown: Voevodsky found modern math was too complicated for anybody including his peers at the IAS to trust outsider research because there were too many problems found in even proofs written by top mathematicians including problems found in his own proofs. Unless you had some prestigious university pedigree nobody would be able to trust your proofs, so nobody even looks at them. In his words modern math is completely broken as a field and the best way to fix this he thought, was computer assisted proofs that way if some unkown mathematician uploaded a paper it would come with all it's proofs as a program you could run and verify it first so you knew you weren't wasting your time.

An enormous amount of mathematicians and type theory specialists were assembled to produce Homotopy Type Theory (see the HoTT book). This was described by Robert Harper to be 'a misadventure in formalisms' who deemed it insufficiently computational, and then this research became Computational Type Theory which is what we are taking here.

There is a very good interview with Voevodsky here:

When I first started to explore the possibility, computer proof verification was almost a forbidden subject among mathematicians. A conversation about the need for computer proof assistants would invariably drift to Gödel’s incompleteness theorem (which has nothing to do with the actual problem) or to one or two cases of verification of already existing proofs, which were used only to demonstrate how impractical the whole idea was.

Per Martin-Lof

A Swedish logician who takes very advanced subjects and breaks them down that anybody at any level can understand. We will read many of his papers here and the book Programming in Martin-Lof's Type Theory which Robert Harper assumes the viewer of this lectures is familiar with.

Robert Harper

Most of our material will consist of his lectures and draft book on Computational Type Theory, and his book PFPL. He also has a Homotopy type theory recorded lecture seminar we may do time allowing because it's great for explaining higher dimensional types. Robert Harper purposely makes his lectures provocative in order to elicit a response in the reviewer to investigate themselves what he's talking about it which is a good strategy. He will hand out very blunt and honest answers, this will be very refreshing.

Let's begin

I guess we should start with the Oregon Programming Language Summer school archive from 2012 as that edition gives category theory lectures, proof theory and type theory lectures together to show they are all describing the same thing which is computation. The notation will explained in the proof theory lectures, the PMLTT book and we can concurrently take a constructive logic course to run this logic as a program.

Intro to Type Theory

This is a great lecture and the most accessible of all his lectures, as it's from the very beginning. 'Something is true only if you have a proof' is different than the typical logic we learn in school where to prove something exists, you can assume it doesn't then show a contradiction so it must exist. @16:30 classic Robert Harper comment about the absolute state of modern PL development.

Interesting definition what a lemma is, or the lemma rule. Meet/Greatest Lower Bound in real analysis is the infimum or inf, the opposite of the supremum or sup and is shown with examples in Tao's Analysis I starting with Example 6.2.8 ie: the set {1,2,3,…} the greatest lower bound is 1, and least upper bound is infinity. If you take an empty set, inf(empty) is infinity, and the sup(empty) is negative infinity, since by definition inf() will move positive to the right on the real number line looking for the 'greatest lower bound' of nothing, while sup() will move negatively left looking for the least upper bound. Since the set is empty and neither exist they just keep on going to infinity in opposite directions.