Homotopy Type Theory Lectures and Notes On-Line

My activity on this blog has been reduced to nil recently because I have been spending my time preparing a series of lectures on homotopy type theory, starting from basic principles and ending with the application of univalence and higher inductive types to algebraic topology.  The course web page contains links to the video-taped lectures and to the course notes prepared by the students this semester.  These will be available indefinitely and are accessible to anyone interested in the course.  My hope is that these will provide a useful introduction to the HoTT Book, which is available for free on the web and may be printed on demand.  My intention is to write an introduction to dependent type theory for a CS audience, which will serve as a reference for much ongoing work in the area and as a prolegomenon to the HoTT Book itself.


2 Responses to Homotopy Type Theory Lectures and Notes On-Line

  1. Thank you for the excellent lectures. They are much more accessible to CS graduates than HoTT book which is hard to read without a lot of math background.

  2. Bogdan Barbu says:

    Thanks. I’ve been keeping a close eye on your blog for a while and lately have been mocking around with Coursera and edX. I kept thinking to myself “It’d be awesome if Robert Harper decided to share lectures to a course on PLT and/or HoTT.” Imagine my reaction when that came true. Thanks, man!

Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: