Proof-Assistant Working Group at ENS de Lyon

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.

Schedule

Future

April 20th, 2026 - Amphi I (ground floor) and online

• 10:30-12:00 Rocq Tutorial #3 (Cyril Cohen) [sources]
• 13:30-14:45 [user talk / Rocq / beginner] Formalizing category theory in Rocq (Samuel Arsac)
• 15:00-16:15 [tooling talk / Rocq] Rocq's Conversion and Reduction Engines (Guillaume Melquiond) [sources]

May 18th, 2026

June 15th, 2026 [cancelled]

Past

March 23rd, 2026

• 10:30-12:00 Rocq Tutorial #2 (Samuel Arsac) [sources]
• 13:30-14:45 [user talk / Rocq] Layers of Confluence for Actors (Ludovic Henrio)
• 15:00-16:15 [tooling talk / Rocq] Inferring list equalities, and more generally, McLane morphisms - continued (Damien Pous) [sources]

February 23rd, 2026

• Rocq Tutorial #1 (Quentin Vermande) [sources]
• [user talk / Rocq] Rocq the sequents (Olivier Laurent) [sources]
• [tooling talk / Rocq] Inferring list equalities, and more generally, McLane morphisms (Damien Pous) [sources]

December 15th, 2025

• [user talk / Rocq / expert] How to prove your mergesort correct and stable (Kazuhiko Sakaguchi)
• [tooling talk / Rocq / expert] Re-unifying Typeclasses and Canonical Structures (Quentin Vermande)

Further information

We are online: streaming - chat.

Please register to the following mailing list to get information about future sessions, news and reminders:
https://listes.ens-lyon.fr/sympa/subscribe/proof-assistants.lip

If you want to contribute a talk, please send a mail to organizers.proof-assistants.lip@ens-lyon.fr