Workshop on Homotopy Type Theory / Univalent Foundations (original) (raw)
June 25-26, 2016, Porto, Portugal
Collocated withFSCD 2016.
Overview
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.
Followinglast 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, …).
Format and schedule
The workshop will include invited and contributed talks, and possibly a discussion session (depending on scheduling and interest).
For practical details, registration, etc., see themain FSCD site.
Slides of the presentations
- Adams*, Polonsky - Type theory with native homotopy universespdf
- Boulier (talk by Tabareau) - Model structures on types in type theorypdf
- Escardo - Compact types and ordinals in univalent type theorypdf
- Hofmann*, Streicher - Splitting dictoses
- Mörtberg - Cubical Type Theory: a constructive interpretation of the univalence axiompdf
- Orton*, Pitts - Modelling Cubical TT in Agda pdf
- Rijke*, Buchholtz - Classifying types pdf
- Van der Weide*, Geuvers, Basold - Higher inductive types pdf
- Van Doorn - HoTT in Lean pdf
- Uemura* - Fibred fibration categories pdf
Submissions
Abstract submission deadline: Wednesday 20 April, 2016.
Submissions should consist of a title and abstract, in pdf or text format, viaEasyChair
Talks on practical formalisation are particularly solicited, but submissions on all UF/HoTT topics are welcome.
Organisers
- Peter LeFanu Lumsdaine,
p.l.lumsdaine at gmail.com(Stockholm University) - Nicolas Tabareau,
nicolas.tabareau at inria.fr(Inria, Nantes)
Program Committee
- Benedikt Ahrens (Institute for Advanced Study, Princeton)
- Steve Awodey (Carnegie Mellon University)
- Thierry Coquand (University of Gothenburg)
- Eric Finster (École Polytechnique)
- Nicolai Kraus (University of Nottingham)
- Peter LeFanu Lumsdaine (Stockholm University)
- Nicolas Tabareau (Inria, Nantes)