Several links related to the type-theoretic formalization
of mathematics:
Several links related to the type-theoretic formalization
of mathematics:
• 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.
• Homepage of Steve Awodey who pioneered the study of the connections
between Martin-Lof identity types, homotopy-theoretic factorization axioms and omega-categories.
• Homepages of Thomas Streicher and Martin Hofmann.