Lifting proof-relevant unification to higher dimensions (CPP 2017) - POPL 2017

Sun 15 - Sat 21 January 2017

Who

Jesper Cockx, Dominique Devriese

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:30 - 15:00 at Auditorium - Homotopy type theory

Jesper Cockx

iMinds, Belgium

Belgium

Dominique Devriese

iMinds - Distrinet, KU Leuven

Belgium

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