/* ** xxhxx -- xxhxx ** · nom · {{lien|titre}} */ /* 10h25 - 10h35 : Manuel Catz 10h35 - 10h45 : Umberto Tarantino 10h45 - 11h15 : Pause café Session 2 11h15 - 11h45 : Rémy Cerda (post-doc) 11h45 - 12h15 : Snow Xuejing Huang (post-doc) 12h15 - 12h25 : Miriam Marzaioli 12h25 - 12h35 : Yves Ndiaye 12h40 - 14h00 : Déjeuner (buffet) Session 3 14h00 - 14h30 : Informations sur PPS 14h30 - 15h00 : Yoann Barszezak (ATER) 15h00 - 15h10 : Eleonore Mangel 15h10 - 15h20 : Enzo Erlich 15h30 - 16h00 : Dominik Kirst (post-doc) Clôture 17h00 : Pot de fin (dans un café) */ ** 09h30 - 10h15 ** · [[https://www.irif.fr/~narboux/|Julien Narboux]] (MCF) · //Theorem Proving as Constraint Solving using Coherent Logic//

I will first give a quick overview of my research interests : automated and interactive proof in geometry, using proof assistant for teaching, then I will focus on recent joint work with Predrag Janičić about the use constraint solving for automatic theorem proving. One of the features of the implemented prover Larus is that it can generate human understandable proofs in natural language and also machine-verifiable proofs for the interactive prover Coq.

** 10h15-10h25 ** · Gaëtan Lopez · TBA ** 10h25 - 10h35 ** · Manu Katz · TBA ** 10h35 - 10h45 ** · Umberto Tarantino · //Triposes and toposes through arrow algebras// // 10h45 — 11h15 : Coffee break // ** 11h15 - 11h45 ** · [[https://www.i2m.univ-amu.fr/perso/remy.cerda/|Rémy Cerda]] (post-doc) · //The missing ingredient in the linear approximation of the λ-calculus//

The somehow pedantic title of this talk hides a simple and very old (yet not fully explored for a long time) idea: The dynamics of β-reduction is intrinsically coinductive. The goal of my PhD thesis was to take this idea seriously in the setting of the linear approximation of the λ-calculus, i.e. to reformulate the Taylor expansion of λ-terms in an infinitary setting. Doing this allows to reorganise many results, including the good old continuous approximation based on approximation orders.
I will conclude this tentative autobiography of a very short scientific life with a few words about other topics I have been, am currently, or would like to be working on -- all gravitating around this idea of infinitary dynamics.

** 11h45-12h15 ** · [[https://xsnow.live|Snow Xuejing Huang]] (post-doc) · Intersection Types for Modular Programming

Calculus with disjoint intersection types supports a symmetric merge operator which generalizes record concatenation. Equipped with distributive subtyping, such a type discipline provides a foundation for Compositional Programming, a new modular style of statically typed programming that features dynamic inheritance, in which solutions to the expression problem arise naturally. In this talk, I will briefly overview the core calculus of disjoint intersection types and explore its design space. During my postdoc, I am studying the module system of Elixir, a dynamic functional programming language. I aim to incorporate it into the recently developed static type system of Elixir—a polymorphic type system with set-theoretic types and semantic subtyping. Semantic subtyping interprets types as sets of values and provides a different understanding of intersection types. My current goal is to explore how to encode the first-class modules in Elixir with existential types and to establish a set-theoretic interpretation for existential types.

** 12h15 - 12h25 ** · Miriam Marzaioli · TBA ** 12h25 - 12h35 ** · Yves Ndiaye · TBA // 12h35 - 14h — Lunch // **14h00 - 14h30 ** · Informations sur PPS **14h30 - 15h00 ** · Yoann Barszezak (ATER) · //On the construction of shapely monads//

TBA

**15h00 - 15h10 ** · Eleonore Mangel · TBA **15h10 - 15h20 ** · [[https://perso.eleves.ens-rennes.fr/people/enzo.erlich/|Enzo Erlich]] · TBA **15h30 - 16h00 ** · [[https://www.ps.uni-saarland.de/~kirst/|Dominik Kirst]] (post-doc) · Mechanised Reverse Mathematics and Related Research Projects

I will give a brief overview of the lines of work I’m currently involved with, that all more or less connect to the mechanisation of (constructive) reverse mathematics in the Coq proof assistant. I’ll focus on the logical analysis of theorems concerning first-order logic and computability theory but will also describe how this analysis motivates studying particular models of intuitionistic higher-order logic and constructive type theory.

// 17h00 — Clôture: Pot de fin (dans un café ou IRIF cake)//