Workshop on Homotopy Type Theory / Univalent Foundations

June 29-30, 2015, Warsaw, Poland

Collocated with RDP/TRA/TLCA 2015.


Homotopy Type Theory/Univalent Foundations is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, informed by ideas and tools from abstract homotopy theory.

One practical goal of the programme is to facilitate computer formalisation of mathematics in such logical systems. We aim to focus on that aspect: bringing together researchers on formalisation in UF/HoTT to discuss the various established and experimental proof assistants for it, the different libraries available (HoTT Coq, Unimath, HoTT-Agda, …), what logical features are convenient for the formalisation of “homotopical mathematics”, and how to make formalisation in HoTT/UF accessible and practical for mathematicians.


You can download abstracts of contributed talks here.


Invited Speakers

Format and schedule

The work shop will include invited talks, contributed talks, and a round-table discussion session.

The discussion topic is the state of libraries and documentation for programming in HoTT using Coq and Agda. We hope to stimulate effort to make the existing resources more accessible, and improve and supplement them where they are lacking, to help new researchers get active in this topic.

For practical details, registration, etc., see the main RDP site.


Abstract submission deadline: April 15, 2015.

Submissions should consist of a title and abstract, in pdf or text format, via EasyChair

Talks on practical formalisation are particularly solicited, but submissions on all UF/HoTT topics are welcome.


Program Committee