Feb 23: Proof Assistant WG at ENS de Lyon

Announcements
1

Dear all,

It is our pleasure to announce the second session of our working group dedicated to proof assistants and their use at ENS de Lyon, two weeks from now. The working group will be hybrid, see the locations at the bottom of the mail.

Detailed schedule for Feb 23rd, 2026

with talks from Quentin Vermande, Olivier Laurent and Damien Pous.

  • 10:30-12:00 tutorial
    Quentin Vermande: an introduction to the Rocq prover.

  • 13:30-14:45 user talk
    Olivier Laurent: Rocq the sequents.

We present design choices and challenges for the formalization in Rocq
of various sequent calculi.
We give an incremental presentation with richer and richer sequent
structures corresponding to richer and richer order structures and
(substructural) logical systems. Starting from (bounded) lattices
(a.k.a. intuitionistic additive linear logic) with Whitman’s
presentation, we visit involutive lattices (a.k.a. classical additive
linear logic), ortholattices (a.k.a. orthologic or minimal quantum
logic), residuated lattices (a.k.a. Lambek calculus) and their
commutative version (a.k.a. intuitionistic multiplicative additive
linear logic), etc.
Cut admissibility (i.e. transitivity admissibility from the order
point of view) is our main focus as a key property we want to
formalize. Among the ingredients to consider in Rocq, we discuss list
manipulations, permutations, Prop vs Type, parameterized inductives,
representation of quantifiers, cut admissibility vs cut elimination,
etc.

  • 15:00-16:15 tooling talk
    Damien Pous: Inferring list equalities, and more generally, McLane morphisms.

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

Schedule of the next working groups.

  • March 23rd, 2026 10:30-12:00 (tutorial), 13:30-14:45 and 15:00-16:15
  • April 20th, 2026 10:30-12:00 (tutorial), 13:30-14:45 and 15:00-16:15

Further information

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

Best wishes,

Cyril Cohen,
on the behalf of the organizing committee of the working group

3 Likes
New proof assistant working group at ENS de Lyon