European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

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