Course imparted by Robert Harper. I believe they are following the Homotopy Type Theory book. See also Harper's blog and the latest edition of his Practical Foundations for Programming Languages book. See also the "proof theory foundations" videos linked in the "So you want to learn type theory... but where to start?" page.