Several links related to the type-theoretic formalization

of mathematics:

 
  1. Programming languages course taught in Princeton in the fall of 2009 using Coq: http://www.cs.princeton.edu/courses/archive/fall09/cos441/

In particular look at “schedule” which contains links to the lecture notes.


  1. Homepage of Steve Awodey who pioneered the study of the connections

between Martin-Lof identity types, homotopy-theoretic factorization axioms and omega-categories.


  1. Homepages of Thomas Streicher and Martin Hofmann.