June 25-26, 2016, Porto, Portugal
Collocated with FSCD 2016.
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.
Following last year's instalment in Warsaw, this workshop will focus again on the practical formalisation of mathematics in HoTT/UF-based style, in computer proof assistants (Coq, Agda, Lean, …).
The workshop will include invited and contributed talks, and possibly a discussion session (depending on scheduling and interest).
For practical details, registration, etc., see the main FSCD site.
Abstract submission deadline: Wednesday 20 April, 2016.
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.
p.l.lumsdaine at gmail.com(Stockholm University)
nicolas.tabareau at inria.fr(Inria, Nantes)