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.
Overview
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.
Speakers
- Robin Adams: Why Is It Still Hard to Formalize Metatheory? (abstract, slides)
- Thierry Coquand: Stack model of type theory (abstract, slides)
- Peter Dybjer: Finitary Higher Inductive Types in the Groupoid Model (abstract, slides)
- Martin Escardo: Partial elements and recursion in univalent type theory (abstract)
- Ambrus Kaposi: Formalisation of the metatheory of type theory using quotient inductive types (abstract, slides)
- Dominique Larchey-Wendling: Kruskal's tree theorem in Type theory (abstract, slides)
- Zhaohui Luo: MTT-semantics and Its Formalisation (abstract, slides)
- Marco Maggesi: De Bruijn Monads (abstract, slides)
- Ralph Matthes: Abstract signatures for substitution systems (abstract, slides)
- Niels van der Weide: The Three-HITs Theorem (abstract, slides)
- Felix Wellen: Formalizing aspects of differential Cohesion in Homotopy Type Theory (abstract, slides)
Program
| 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.
Practicalities
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.
Accommodation
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.
Organiser
Links