The HoTT library: a formalization of homotopy type theory in Coq (CPP 2017) - POPL 2017

Sun 15 - Sat 21 January 2017

Who

Andrej Bauer, Jason Gross, Peter Lefanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters

Track

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

Tue 17 Jan 2017 14:00 - 14:30 at Auditorium - Homotopy type theory

Link to Preprint

https://arxiv.org/abs/1610.04591

Andrej Bauer

University of Ljubljana

Slovenia

Jason Gross

MIT CSAIL

United States

Peter Lefanu Lumsdaine

Michael Shulman

Matthieu Sozeau

Inria

France

Bas Spitters

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

	14:00 - 15:30	Homotopy type theoryCPP at Auditorium

	14:00 30m Talk		The HoTT library: a formalization of homotopy type theory in Coq CPP Andrej Bauer University of Ljubljana, Jason Gross MIT CSAIL, Peter Lefanu Lumsdaine , Michael Shulman , Matthieu Sozeau Inria, Bas Spitters Pre-print
	14:30 30m Talk		Lifting proof-relevant unification to higher dimensions CPP Jesper Cockx iMinds, Belgium, Dominique Devriese iMinds - Distrinet, KU Leuven
	15:00 30m Talk		The Next 700 Syntactical models of type theory CPP Simon Boulier , Pierre-Marie Pédrot , Nicolas Tabareau Inria, France