Dear all,
It is our pleasure to announce the third session of our working group dedicated to proof assistants and their use at ENS de Lyon, next week from now. The working group will be hybrid, see the locations at the bottom of the mail.
Detailed schedule for March 23rd, 2026
with talks from Samuel Arsac, Ludovic Henrio and Damien Pous.
- 10:30-12:00 Tutorial
Samuel Arsac: The Rocq prover. - 13:30-14:45 User talk
Ludovic Henrio Layers of Confluence for Actors
This paper introduces a novel proof technique to show that parallel or distributed programs exhibit confluent behavior, even when the execution of these programs is inherently non-deterministic. The proposed method allows us to prove the confluence of programs for which standard properties such as strong confluence or commutativity of operations do not hold. Our technique builds on a method to prove the confluence of rewrite systems by de Bruijn, which we first adapt and formalize in Rocq. This method can be seen as a specialized induction principle for proving confluence. The paper further considers how this induction principle can be used in the context of programming languages. We show how the proof method can be instantiated to establish confluence conditions for programs in a small Actor-like programming language and demonstrate the application of the method to prove the confluence of a class of programs that cannot be proven to have deterministic behaviours by standard techniques.
- 15:00-16:15 Tooling talk
Damien Pous: Inferring list equalities, and more generally, McLane morphisms. - continued
Dealing with associativity in the free monoid of lists is boring.
Similarly, writing explicit reassociators between tensor expressions in monoidal categories is painful.
I will show how to automate this process in Rocq, using canonical structures and reflection.
This makes it possible to setup concise notations for monoidal categories, and then to interface with graphical tools working at the level of string diagrams.
Location
- Amphi I (ground floor), ENS de Lyon (site Monod), 46 allée d’italie 69007 Lyon
- Webinaire de l'État
Schedule of the next working groups.
- April 20th, 2026 10:30-12:00 (tutorial), 13:30-14:45 and 15:00-16:15
Further information
Please register to the following channels to get information about future sessions, news and reminders:
- proof-assistants.lip - Newsletter for the working - subscribe
- Public view of The Rocq Prover | Zulip team chat
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