Workshop on Homotopy Type Theory/ Univalent Foundations

September 8-9, 2017, Oxford, United Kingdom.

Co-located with FSCD 2017.

Quick info

Location: Department of Computer Science, OERC Building, 7 Keble Road (Google map)
Link to the programme
For speakers: the room is equiped with a computer and projector, as well as with a whiteboard that can be used in parallel with the projector. We recommend you bring your slides on a USB memory stick. If you prefer, HDMI and VGA connectors are available to hook up your laptop to the projector.

Overview

Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory.

The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory/Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. As part of the workshop there will be an introductory tutorial intended to make the invited and contributed talks accessible to non-experts.

Format

The workshop will include a tutorial, invited and contributed talks, and possibly a discussion session (depending on scheduling and interest).

For details regarding registration and accommodation see the corresponding FSCD site. FSCD also provides some student funding with application deadline July 21. For all other practical details see the main FSCD site.

Invited speakers

Thorsten Altenkirch (University of Nottingham):
Naïve Type Theory (tutorial)
Ulrik Buchholtz (Technical University of Darmstadt):
Formalizing type theory in type theory using nominal techniques [slides]
Thierry Coquand (University of Gothenburg):
Sheaf models for univalent type theory [slides]

Program

The schedule can be found here. Titles and abstracts of the contributed talks can be found below:

Danil Annenkov, Paolo Capriotti and Nicolai Kraus:
Formalisations Using Two-Level Type Theory
(abstract | slides)
Simon Boulier and Nicolas Tabareau:
Model Structure on the Universe in a Two Level Type Theory
(abstract | slides)
Simon Boulier, Egbert Rijke and Nicolas Tabareau:
A coinductive approach to type valued equivalence relations
(abstract | slides)
Simon Cho, Cory Knapp, Clive Newstead and Liang Ze Wong:
Weak equivalences between categories of models of type theory
(abstract)
Cesare Gallozzi:
Homotopy Type-Theoretic Interpretations of CZF
(abstract | slides)
Robert Graham:
Synthetic Homology in Homotopy Type Theory
(abstract)
Jacob A. Gross, Daniel R. Licata, Max S. New, Jennifer Paykin, Mitchell Riley, Michael Shulman and Felix Wellen:
Differential Cohesive Type Theory
(abstract | slides1 slides2)
Egbert Rijke, Michael Shulman and Bas Spitters.
Modalities in homotopy type theory
(abstract | slides)
Andrew Swan:
Lifting Problems in a Grothendieck Fibration
(abstract | slides)
Andrea Vezzosi:
Adding Cubes to Agda
(abstract)
Matthew Weaver and Dimitris Tsementzis:
Unfolding Folds
(abstract | slides)
Jonathan Weinberger and Thomas Streicher:
Interpreting type theory in appropriate presheaf toposes
(abstract | slides)

Submissions

Submissions should consist of a title and a 1-2 pages abstract, in pdf format, via EasyChair.

Abstract submission deadline: June 30
Author notification: mid July

Considering the broad background of the expected audience, we encourage authors to include information of pedagogical value in their abstract, such as motivation and context of their work.

Organisers

Benedikt Ahrens, benedikt.ahrens at inria.fr (Inria Nantes)
Simon Huber, simon.huber at cse.gu.se (University of Gothenburg)
Anders Mörtberg, anders.mortberg at inria.fr (Inria Sophia-Antipolis)

Program committee

Benedikt Ahrens (Inria Nantes)
Paolo Capriotti (University of Nottingham)
Simon Huber (University of Gothenburg)
Chris Kapulkin (University of Western Ontario)
Peter LeFanu Lumsdaine (Stockholm University)
Assia Mahboubi (Inria Saclay)
Anders Mörtberg (Inria Sophia-Antipolis)
Paige North (University of Cambridge)
Nicolas Tabareau (Inria Nantes)

Special issue

We are soliciting submissions for a Special Issue of the journal

Mathematical Structures in Computer Science
(Cambridge University Press)

edited in association with the 2017 and 2018 editions of the HoTT/UF workshop. Submissions based on work presented at the HoTT/UF'17 workshop are particularly welcome, but submission is open to everyone and not limited to workshop participants. More information can be found here.