Workshop on Foundations for the practical formalization of mathematics (FPFM)

April 26–27, 2017, Nantes, France

Meeting in the framework of the COST Action EUTypes.


Proof assistants are now state of the art tools for formalizing mathematical reasoning, both for the verification of proofs in mathematics itself and for the verification of software and hardware in computer science. Various proof assistants are based on type theory and it turns out that powerful type theory provide a rich language for capturing notions from computer science and mathematics, ranging from very algorithmic notions (correctness of programs) to very abstract mathematics like homotopy theory (due to the recent advances in Homotopy Type Theory).

For this workshop we have invited researchers in formalizing mathematics and proof assistants based on dependen type theory, homotopy type theory, higher inductive types and cubical type theory, to discuss how type-based proof assistant can be used for the practical formalization and verification of mathematical proofs.



Wednesday, 26 April
10:30 - 11:15 Tea
11:20 - 12:10 Maggesi
12:10 - 13:00 Matthes
13:00 - 15:00 Lunch break
15:00 - 15:50 Dybjer
15:50 - 16:40 van der Weide
16:40 - 17:10 Tea
17:10 - 18:00 Luo
20:00 - Dinner
Thursday, 27 April
09:50 - 10:40 Wellen
10:40 - 11:15 Tea
11:20 - 12:10 Coquand
12:10 - 13:00 Larchey-Wendling
13:00 - 15:00 Lunch break
15:00 - 15:50 Adams
15:50 - 16:40 Escardo
16:40 - 17:10 Tea
17:10 - 18:00 Kaposi

Information about dinner on Wednesday, 26 April, will be provided in due course.


The workshop takes place at IMT Atlantique, on the outskirts of Nantes.

How to get to IMT Atlantique?

To get to IMT Atlantique from the city center of Nantes, take the bus C6 in the direction of Chantrerie. Get off the bus at the stop Chantrerie. From the bus stop, it is a 4-minute walk to IMT Atlantique: see the plan (Google Maps) for directions.
You need to validate your ticket upon entering the bus, by putting it into a tiny machine at the entrance of the bus. A ticket is valid for one hour, unlimited transfers. You need to validate your ticket every time you enter a bus, even if you have validated it before.
Tickets bought at a ticket machine are 1.60EUR. Tickets bought in the bus are 2EUR, and exact change might be needed.
Be aware that Google Maps does not show public transportation timetables for Nantes. Instead, you should use the website of the public transportation organisation, TAN.

Information on the workshop room

The workshop takes place in room J156/158 at IMT Atlantique. The room is equipped with a whiteboard, whose center part also serves as a surface to project slides. The whiteboard also has two wing parts, which can be written onto in parallel to projecting onto the center part.
The room has sufficiently many electric sockets.

How to travel between the city center and the airport?

A shuttle bus runs between the city center and the airport. A ticket is 8.50EUR and is valid one hour from the start of your journey, including transfers.


Since it is necessary to take the bus C6 to IMT Atlantique, I recommend choosing a hotel that is close to a C6 stop.
Unfortunately, Google Maps does not show the public transportation of Nantes, so you need to check against this plan instead. C6 is the light purple line going north-north-east from the city center. (Hovering over a line will show its name.)
Below is a list of hotels that are not far from a bus stop of line C6.