CoREACT General Meeting Winter 2025

IRIF - Université Paris Cité, Bâtiment Sophie Germain, salle 3052 and 3063

Date
December 19, 2025 10:00 — 17:00
Location
IRIF (salle 3052 and 3063)

Organisation

The meeting will be held in hybrid mode, i.e., both via Zoom and in the form of in-person meetings at IRIF (Salle 3052 and 3063).

Program

Please note: the first afternoon session will take place in Salle 3063, while all other sessions will take place in the main seminar room on the third floor of IRIF (Salle 3052).

Time Speaker Title
10:00 - 10:05 Kazuhiko Sakaguchi Introduction of the IC Rocq workgroup
10:05 - 10:30 Samuel Arsac Adhesive Category Theory for Graph Rewriting in Rocq
10:30 - 10:45 Samuel Arsac On Computable (Co-) Equalizers
10:45 - 11:30 Manuel Catz Diagrammatic (Proofs in) Rocq
12:00 - 12:30 Kazuhiko Sakaguchi Tactics Modulo Associativity and Cancellation for Category Theory
12:30 - 13:00 Nicolas Behr Conditional Hyperdoctrines - An Update
14:00 - 15:00 discussion on proof data management/UI design/CoREACT wiki
15:30 - 17:00 discussion on formalization/implementation of Instantiation Calculus in Rocq