Equations: a tool for dependent pattern-matching (TTT 2017) - POPL 2017

Sun 15 - Sat 21 January 2017

Who

Cyprien Mangin, Matthieu Sozeau

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

Sun 15 Jan 2017 14:50 - 15:10 at Salle 105, Barre 44-54 - First Afternoon Session Chair(s): Bas Spitters

File attachments

Abstract (abstract.pdf)	115KiB

Cyprien Mangin

Matthieu Sozeau

Inria

France

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

Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

	14:00 - 15:30	First Afternoon SessionTTT at Salle 105, Barre 44-54 Chair(s): Bas Spitters

	14:00 50m Talk		Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom TTT Anders Mörtberg Inria
	14:50 20m Talk		Equations: a tool for dependent pattern-matching TTT Cyprien Mangin , Matthieu Sozeau Inria File Attached
	15:10 20m Talk		Coq's Prolog and application to defining semi-automatic tactics TTT Théo Zimmermann IRIF, Université Paris Diderot, Hugo Herbelin File Attached