==== Programme ====

<panel title="Lundi 28 novembre · Amphithéâtre Alan Turing, Bâtiment Sophie Germain">

//10h — Accueil des participants//

**10h30-12h30 · Session 1**
  * 10h30-11h15 — Emmanuel Beffara · {{beffara.pdf|Describing processes and their executions in proof theory}}
  * 11h15-11h40 — Lionel Vaux · {{vaux.pdf|Infinitary normal forms for non-deterministic $\lambda$-terms}}
  * 11h40-12h05 — Charles Grellois · {{grellois.pdf|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 · {{keller.pdf|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 · {{durier.pdf|Unique solutions of equations in process calculi}}

//Pause-café//

**17h-19h30 · Session 3**
  * 17h-17h25 — Daniel El Ouraoui · {{el-ouraoui.pdf|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)//

</panel>

<panel title="Mardi 29 novembre · Salle des thèses, Halle aux Farines (hall F)">

**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 · {{vial.pdf|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 · {{lozes.pdf|On the Relationship Between Higher-Order Recursion Schemes and Higher-Order}}

//Déjeuner (buffet sur place)//

**14h-15h35 · Session 6**
  * 14h-14h45 — Samuel Mimram · {{mimram.pdf|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 · {{delcroix-oger.pdf|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//

</panel>