Programme Lundi 28 novembre · Amphithéâtre Alan Turing, Bâtiment Sophie Germain 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) 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 · 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