HoTT/UF 2016
source link: http://hott-uf.gforge.inria.fr/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Workshop on Homotopy Type Theory / Univalent Foundations
June 25–26, 2016, Porto, Portugal
Collocated with FSCD 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.
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, …).
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 the main FSCD site.
Slides of the presentations
- Adams*, Polonsky – Type theory with native homotopy universes pdf
- Boulier (talk by Tabareau) – Model structures on types in type theory pdf
- Escardo – Compact types and ordinals in univalent type theory pdf
- Hofmann*, Streicher – Splitting dictoses
- Mörtberg – Cubical Type Theory: a constructive interpretation of the univalence axiom pdf
- 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, via EasyChair
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)
Archives
Last modified: Fri Jul 1 10:18:40 CEST 2016
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK