Higher-Dimensional Type Theory Seminar

WHAT? This lecture series conducted by Bob Harper will cover various topics in higher-dimensional type theory, including higher category theory and homotopy theory. It is not for the faint of heart.

WHO? This is some hardcore PL stuff. You should know dependent type theory and at least some category theory.

WHEN? See schedule below.

WHERE? MPI-SWS Kaiserslautern/Wartburg

HOW? Mailing list for this series (and other type theory discussion): type-theory@mpi-sws.org

Organizers: Bob Harper and Scott Kilpatrick

Videos: The videos of lectures 2-4 are available online. Altogether they're around 850mb. Use VLC to play them if you're having trouble. They're password protected; email Scott for the credentials.

Schedule

1

2011-08-03, 2PM

SB

Intro to HDTT and homotopy.

2

2011-08-05, 1PM

SB

Intro to dependent type theory and equality types.

3

2011-08-10, 1PM

SB

More on equality in dependent type theory.

4

2011-08-19, 1PM

SB

Univalence, 2DTT, inductive definitions, and concluding remarks.

Resources

Blogs and Websites

Papers

Topics

Meeting #1

Meeting #2

Meeting #3

Meeting #4

hdtt (last edited 2011-08-24 15:58:47 by skilpat)