Inter-WG developers meeting, Le Val d’Ajol, 24-26 September 2025
Organizer: Frédéric Blanqui
Date: 24-26 September 2025
Venue: La Résidence, 5 rue des Mousses, 88340 Le Val d’Ajol, France
Participants (15): Frédéric Blanqui, Abdelghani Alidra, Bruno Barras, Benjamin Thibaut, Ewen Broudin-Caradec, Catherine Dubois, Ciarán Dunne, Olivier Hermant, Nicolas Margulies, Melanie Taprogge, Thomas Traversié, Rishikesh Vaishnav, Théo Winterhalter, Antoine Gontard, Ivan Martinez Comas.
Wednesday 24 September:
| 13:00-14:30 | lunch |
| 14:30-16:30 | work session 1 |
| 16:30-17:00 | coffee break |
| 17:00-19:00 | work session 2 |
| 19:00-20:00 | free time |
| 20:00-21:30 | dinner |
Thursday 25 September:
| 08:30-09:00 | breakfast |
| 09:00-10:30 | work session 3 |
| 10:30-11:00 | coffee break |
| 11:00-13:00 | work session 4 |
| 13:00-14:30 | lunch |
| 14:30-16:30 | work session 5 |
| 16:30-17:00 | coffee break |
| 17:00-19:00 | work session 6 |
| 19:00-20:00 | free time |
| 20:00-21:30 | dinner |
Friday 26 September:
| 08:30-09:00 | breakfast |
| 09:00-10:30 | work session 7 |
| 10:30-11:00 | coffee break |
| 11:00-13:00 | work session 8 |
| 13:00-14:30 | lunch |
Program:
- work session 1:
- organization of the meeting
- discussion on next seminars
- talk by Ivan Martinez Comas: algebraic effects in pure subtyping systems
- work session 2:
- individual work
- initiation to lean2dk and lean4less by Rish
- work session 3:
- individual work
- discussion on the conservativity of Lean over Lean-
- work session 4:
- individual work
- initiation to Lambdapi by Frédéric
- work session 5:
- round table (part 1): mini-talks by every participant
- Bruno Barras: Coqine, rewriting modulo AC
- Ewen Broudin-Caradec: ghost types
- Catherine Dubois: formalization of the A* algorithm on graphs
- Ciarán Dunne: Eo2lp: translator from Eunoia to Lambdapi
- Nicolas Margulies: cubical type theory
- Melanie Taprogge: certification of LEO-III proof traces in Lambdapi
- Rishikesh Vaishnav: explicitation of proof irrelevance in Lean
- Théo Winterhalter: local rewriting in type theory
- round table (part 1): mini-talks by every participant
- work session 6:
- talk by Antoine Gontard: tactics to automatically proving the alignments of inductive type and recursive function definitions
- individual work
- work session 7:
- round table (part 2): mini-talks by every participant
- Abdelghani Alidra: online search engine for libraries translated in Dedukti or Lambdapi (joint work with Claudio Sacerdoti Coen)
- Thomas Traversié: theory morphisms (joint work with Florian Rabe)
- Olivier Hermant: extension of Barr theorem to higher-order logic (joint work with Thomas Traversié and Marc Aiguier)
- talk by Benjamin Thibaut: Generating Higher Identity Proofs in Homotopy Type Theory
- round table (part 2): mini-talks by every participant
- work session 8:
- discussion on the future of the project
- discussion on software maintenance