Presented By: Logic Seminar - Department of Mathematics
Type theory seminar: The Curry-Howard correspondence
Patrick Lutz
This is a learning seminar on dependent type theory, following Egbert Rijke's book "Introduction to Homotopy Type Theory." This talk will cover chapter 7 of Rijke's book, on using the Curry-Howard correspondence to formalize math within type theory.