HDRA 2015 - International Workshop on Higher-Dimensional Rewriting and Applications (HDRA)

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 HoTT/UF 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.
Proposed format and agenda
We plan to hold a round table to discuss on the state of documentation for programming in HoTT in 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 to get active in this topic.
Morning 1: one or two tutorial lectures; then a short round-table on the idea of an introductory book.
Afternoon 1: contributed talks.
Morning 2: one tutorial lecture; a longer round-table to work out details for previous day’s ideas.
Afternoon 2: contributed talks.