22nd Estonian Winter School in Computer Science (EWSCS)
XXII Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 5 - 10, 2017

Thorsten Altenkirch

School of Computer Science
University of Nottingham
United Kingdom

Introduction to homotopy type theory

Abstract

Homotopy type theory is a new foundation of mathematics that generalizes Martin-Löf type theory to higher dimensions, that is non-trivial equality types. It introduces some new basic principles, such as the univalence axiom, which identifies isomorphic types. It also enables us to conduct an abstract version of homotopy theory which has exciting but largely unexplored applications to dependently typed programming. The course builds on the HoTT book, but will also cover some more recent developments like cubical type theory.

Course materials

Valid CSS! Valid XHTML 1.0 Strict Last changed April 7, 2017 19:16 Europe/Helsinki (GMT +03:00) by local organizers, ewscs17(at)cs.ioc.ee
EWSCS'17 page: http://cs.ioc.ee/ewscs/2017/