10h — Accueil des participants

10h30-12h30 · Session 1

• 10h30-11h15 — Emmanuel Beffara · Describing processes and their executions in proof theory
• 11h15-11h40 — Lionel Vaux · Infinitary normal forms for non-deterministic $\lambda$-terms
• 11h40-12h05 — Charles Grellois · Probabilistic termination by monadic sized affine typing
• 12h05-12h30 — Claudia Faggian · The geometry of probabilistic and quantum parallelism

Déjeuner (buffet au 3e étage du bâtiment Sophie Germain)

14h30-16h30 · Session 2

• 14h30-15h15 — Chantal Keller · Interoperability between proof systems: the triumvirate of automation, expressivity, and safety
• 15h15-15h40 — Ralph Matthes · Terms with binding in UniMath: from signatures to monads, without built-in inductive types
• 15h40-16h05 — Sonia Marin · Focused emulation of modal proof systems
• 16h05-16h30 — Adrien Durier · Unique solutions of equations in process calculi

Pause-café

17h-19h30 · Session 3

• 17h-17h25 — Daniel El Ouraoui · Substitutions explicites linéaires et préservation de la normalisation forte: une formalisation en Coq
• 17h25-17h50 — Thibaut Balabonski · Appel par nécessité en réduction forte
• 18h-19h30 — Réunion Géocal-LAC

20h — Dîner (au restaurant Dans la cuisine, devant le bâtiment Sophie Germain)

9h15-10h50 · Session 4

• 9h15-10h — Pierre-Louis Curien · Opérades cycliques, arbres non enracinés et cohérence
• 10h-10h25 — Delia Kesner · Quantitative types for the lambda-mu calculus
• 10h25-10h50 — Pierre Vial · Coinductive Intersection Types are Completely Unsound

Pause-café

11h15-12h30 · Session 5

• 11h15-11h40 — David Baelde, Guilhem Jaber ou Alexis Saurin · Cut-elimination in infinitary proof systems
• 11h40-12h05 — Amina Doumane · Towards Completeness via Proof Search in the Linear Time mu-calculus
• 12h05-12h30 — Étienne Lozes · On the Relationship Between Higher-Order Recursion Schemes and Higher-Order

Déjeuner (buffet sur place)

14h-15h35 · Session 6

• 14h-14h45 — Samuel Mimram · Invariants homologiques pour les théories algébriques
• 14h45-15h10 — Clément Alleaume · Cohérence par réécriture en théorie des représentations
• 15h10-15h35 — Bérénice Delcroix-Oger · Réécriture et opérades

Pause-café

16h-16h50 · Session 7

• 16h-16h25 — Thomas Seiller · Computational Complexity: Between Algebra and Geometry
• 16h25-16h50 — Beniamino Accattoli · A Taste of COCA HOLA

17h — Clôture des journées