9h30 - 10h30 : Audio-conférence avec Mathieu Boesflug.
1. Choix du futur nom d'Europa.
Trans Prover Express ne convient pas à Gilles.
Autres possibilités: Pruvo ou Dedukti.
Dedukti se dégage.

2. Préparation de la realease de Dedukti/Pruvo pour le 30 septembre 2009.
Diffusion proches collaborateurs.
Encore du travail sur le temps de compilation (pour la release de printemps).

3. Collaboration envisagée avec Chantal Keller pour l'exportation
De preuves HOL-Light en Dedukti.

4. Site Web de Dedukti en cours de préparation.

5. Release de traducteurs PA -> Dedukti prévue pour mars 2010.

10h30 - 12h30 : Cody Roux: Program extraction from Gentzen's proof of transfinite induction up to epsilon0 (papier de Ulrich Berger)

14h00 - 14h15 : Paul Brauner: encodage de fold/unfold dans Dedukti

14h15 - 15h30 : Alberto Naibo: Logical Constants from a rewriting point of view

15h45 - 16h45 : Chantal Keller: importation de preuves HOL-Light en Coq

16h45 - 17h30 : Guillame Burel: point sur la traduction de Coq en Dedukti

17h30 - 18h00 : point sur les stages