WG1+2+4 meeting
Organizers: Frédéric Blanqui and Olivier Hermant
Date: 26-27 September 2024
Venue: Ecole des Mines, 35 rue Saint-Honoré, Fontainebleau, France
Participants (15): Bruno Barras, Catherine Dubois, Frédéric Blanqui, Olivier Hermant, Guillaume Burel, Luc Chabassier, Rishikesh Vaishnav, Théo Winterhalter, Thiago Felicissimo, Thomas Traversié, Abdelghani Alidra, Anne Grieu, Melanie Taprogge, Salwa Tabet Gonzalez, Tomaz Mascarenhas
Thursday 26 September:
| 09:30-10:00 | welcome coffee |
| 10:00-10:45 | Encoding of Atelier B proofs in Lambdapi, Anne Grieu |
| 10:45-11:30 | Certification of Leo-III proofs in Lambdapi, Melanie Taprogge |
| 11:30-13:00 | lunch |
| 13:00-13:45 | Progress on Lean4Less, Rishikesh Vaishnav |
| 13:45-14:15 | Ghost types and equality reflection, Théo Winterhalter |
| 14:15-14:45 | Dedukti modulo theories, Bruno Barras |
| 14:45-16:00 | discussion session |
| 16:00-16:30 | break |
| 16:30-18:30 | work session in small groups |
| 18:30-19:30 | break |
| 19:30-21:30 | dinner |
Friday 27 September:
| 09:00-09:30 | Alignment of concepts in Logipedia: some experiments in Coq and Lambdapi, Salwa Tabet Gonzalez |
| 09:30-10:15 | Generic translations between Dedukti theories, Thomas Traversié |
| 10:15-11:00 | Alignment of real numbers between HOL-Light and Coq, Frédéric Blanqui |
| 11:00-12:30 | discussion session |
| 12:30-13:30 | lunch |
| 13:30-14:00 | Adaptation of coq-lsp to Lambdapi, Abdelghani Alida |
| 14:00-14:30 | Tool for graphical category proofs, Luc Chabassier |
| 14:30-15:00 | Deskolemization, Olivier Hermant |
| 15:00-15:30 | Representation of automated proofs in Lambdapi using GDV-LP, Guillaume Burel |
| 15:30-16:00 | break |
| 16:00-17:30 | discussion session |