Organizers: Gilles Dowek, Frédéric Blanqui and Olivier Hermant

Date: 26-27 September 2023

Venue: Ecole des Mines, 35 rue Saint-Honoré, Fontainebleau, France

Programme: Discussing the current status of proof translation tools and libraries, and what to do and how to organize ourselves in the coming years.

Participants (21): Alessio Coltellacci, Anthony Bordg, Bruno Barras, Catherine Dubois, Claude Stolze, Frédéric Blanqui, Gilles Dowek, Olivier Hermant, Guillaume Burel, Louise Dubois de Prisque, Luc Chabassier, Rishikesh Vaishnav, Théo Winterhalter, Thiago Felicissimo, Thomas Traversié, Amélie Ledein, Yoan Géran, Abdelghani Alidra, Wojciech Loboda, Valentin Blot, Nicolas Margulies

Tuesday 26 September:

10:30-10:45 arrival
10:45-11:30 Alethe to Dedukti
11:30-12:15 set theory
12:15-14:00 lunch
14:00-14:45 type universes
14:45-15:45 make implicit conversion explicit
15:45-16:15 break
16:15-17:00 effective translation of libraries
17:00-18:00 discussion on the group organization
18:00-19:00 meetings of senior researchers and junior researchers
19:30-21:30 dinner

Wednesday 27 September:

09:00-10:30 discussion on software development and maintenance
10:30-11:00 break
11:00-11:45 arithmetic
12:00-14:00 lunch
14:00-14:45 cubical type theory
14:45-15:30 semantics of programming languages
15:30-16:00 break
16:00-16:45 categorical proofs
16:45-17:30 scientific report