April 20: Proof Assistant Seminar at ENS de Lyon

Announcements
1

Dear all,

It is our pleasure to announce the fourth session of our working group dedicated to proof assistants and their use at ENS de Lyon, next week from now. The working group is hybrid, see the locations at the bottom of the mail.

Detailed schedule for April 20th, 2026

with talks from Cyril Cohen, Samuel Arsac, and Guillaume Melquiond.

  • 10:30-12:00 Tutorial
    Cyril Cohen: The Rocq prover.

  • 13:30-14:45 User talk
    Samuel Arsac Formalizing category theory in Rocq

I will present a formalization of category theory in Rocq,
discussing the implementation choices made along the way with
a focus on the following points:

  • some details about writing elementary definitions,
  • handling equalities using setoids,
  • organizing a hierarchy of definitions with Hierarchy Builder.
    This talk aims to be beginner-friendly, both in Rocq and
    in category theory.

During this talk, I will focus on proofs by computations. In
particular, I will present the lazy conversion machinery used by the
Rocq kernel during type checking, as well as its two optimized
reduction engines (vm_compute, native_compute). I will also give an
overview of the primitive datatypes (int, float, array, string).
Finally, I will present a few tricks about accessibility predicates,
memoization, etc.

Location

  • Amphi I (ground floor), ENS de Lyon (site Monod), 46 allée d’Italie 69007 Lyon
  • Webinaire de l'État

Further information

Please register to the following channels 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

New proof assistant working group at ENS de Lyon