Dear all,
I have the pleasure to announce the creation of a working group dedicated to proof assistants and their use at ENS de Lyon.
Depending on the sessions, it will target audiences from novices to experts, and may involve different proof assistants: we will strive to tag talks with the appropriate markers.
Here is a preliminary schedule of the upcoming working group.
**December 15th, 2025**
Location: Monod MGN1 109 (may change)
10:30-12:00 Kazuhiko Sakaguchi: How to prove your mergesort correct and stable [expert, Rocq]
14:00-15:30 Quentin Vermande: Re-unifying Typeclasses and Canonical Structures [expert, Rocq]
Abstracts and registration at Answer the survey - Proof assistant meeting Dec 15, 2025 - Evento
According to answers, we may also stream it online.
Next dates will all start with a tutorial session on the Rocq prover:
**Feb 23rd, 2026** 10:30-12:00, 13:30-14:45 and 15:00-16:15
**March 23rd, 2026** 10:30-12:00, 13:30-14:45 and 15:00-16:15
**April 20th, 2026** 10:30-12:00, 13:30-14:45 and 15:00-16:15
Please register to the following mailing list to get information about future sessions, news and reminders:
If you want to contribute a talk, please send a mail to
organizers.proof-assistants.lip@ens-lyon.fr
Best wishes,
Cyril Cohen,
on the behalf of the organizing committee of the working group