The IRIF Laboratory Council, meeting on March 3, 2026, wishes to express its support for the Stand Up for Science movement. The following motion was adopted unanimously by those present. In the face of current threats to academic freedom, sustainable research funding, peer review, and academic democracy, the scientific community is mobilizing through the Stand Up for Science initiative, inspired by the situation of our colleagues in the United States. IRIF joins this movement to promote rigorous, international, and independent research, democratically organized and sustainably funded. Today, such research is being put at risk, in the United States, in France, and elsewhere in the world, by various dangers: Personal attacks against scientists and academics, censorship, pressure, or threats Disinformation and challenges to established scientific facts A reduction in positions and resources, and an excessive steering of funding decisions by public authorities without the involvement of the scientific community. This mobilization aims to remind us that science forms a fundamental pillar of democracy and a guarantee of our collective future. Welcome IRIF is a research laboratory of CNRS and Université Paris Cité, also hosting one Inria project-team. The research conducted at IRIF is based on the study and understanding of the foundations of all computer science, in order to provide innovative solutions to the current and future challenges of digital sciences. IRIF hosts about 200 people. Seven of its members have been distinguished by the European Research Council (ERC), six are members of the Institut Universitaire de France IUF), two are members of the Academia Europæa, and one is member of Académie des sciences. Notion of the day Social Networks Follow us on Twitter/X, LinkedIn and Mastodon for our latest news: News 20.4.2026 Clément Allain, Gabriel Scherer (IRIF, Evidence, Programs and Systems Unit) and their team's work on Snapshottable Stores was featured as an ACM Sigplan Research Highlight in March 2026. Congratulations! 17.4.2026 Congratulations to Cristina Sirangelo and Leonid Libkin (IRIF, Automata Team) whose recent work on the Rel language received the ACM SIGMOD Research Highlight Award. </div> /* news produced automatically from /var/www/dw/data/pages/en/actualites/sources/2026-04-13-conference_undone_computer_science.txt sorting priority 1 */ 13.4.2026 An article in Le Monde is dedicated to the Undone Computer Science conference. Two people from IRIF: Luc Pellissier (IRIF delegation) and Nikolas Melissaris (IRIF) gave presentations there. /* news produced automatically from /var/www/dw/data/pages/en/actualites/sources/2026-04-09-sergio_rajsbaum.txt sorting priority 0.66 */ 9.4.2026 We are pleased to announce the arrival of a new member of IRIF, Sergio Rajsbaum, who has successfully passed the CNRS external research director competition and has been assigned to IRIF in the distributed computing team. Welcome, Sergio. /* news produced automatically from /var/www/dw/data/pages/en/actualites/sources/2026-03-20-nomination_de_claire_mathieu_a_la_commission_d_examen_des_candidatures_a_la_fonction_de_president_du_cnrs.txt sorting priority 0.33 */ 20.3.2026 Claire MATHIEU (IRIF) is appointed as a member of the candidate review committee for the position of president of the National Centre for Scientific Research (CNRS). /* news produced automatically from /var/www/dw/data/pages/en/actualites/sources/2026-02-27-distinguished_talk___javier_esparza.txt sorting priority 0.33 */ 27.2.2026 The IRIF is pleased to announce its first Distinguished Talk of 2026! Our guest speaker is Javier Esparza from the Technical University of Munich. This Distinguished Talk will focus on “Efficient Interactive Proof Protocols for Automated Reasoning.” IRIF Distinguished Talks are open to everyone interested ! /* news produced automatically from /var/www/dw/data/pages/en/actualites/sources/2026-03-06-offre_d_emploi.txt sorting priority 0.33 */ 6.3.2026 Irif is recruiting a new financial and administrative manager (technician level). Position available from May 2026 at the earliest. /* news produced automatically from /var/www/dw/data/pages/en/actualites/sources/2026-03-26-amazon_research_awards_-_geoffroy_couteau.txt sorting priority 0.33 ***/ 26.3.2026 Congratulations to Geoffroy Couteau for his Amazon Research Award on his proposal on « Pseudorandom Correlations for Threshold Cryptography » (AWS Cryptography). edit all the past news (These news are displayed using a randomized-priority ranking.) Agenda Formath Monday April 27, 2026, 2PM, 3052 (+visio) Benno Van Den Berg (ILLC, Universiteit van Amsterdam) Axiomatic Type Theory Homotopy type theory has put the spotlight on the role of equality in type theory. Key is the distinction between propositional and definitional equality. But what roles do these notions of equality play - and what roles should they play? To help answer these questions, I will discuss “axiomatic type theory” (ATT), a version of type theory without the notion of definitional equality. I imagine this to be a system like Book HoTT (so with function extensionality, perhaps univalence and some higher inductive types), where each of the computation rules (including that for the identity type itself) is replaced by a propositional equality. I will discuss properties of ATT, its (natural) categorical semantics and some open questions. Algorithms and complexity Wednesday April 29, 2026, 11AM, Salle 3052 Maud Szusterman (University of Warsaw) New upper bound on the complexity of the matching polytope Type theory and its implementation Wednesday April 29, 2026, 2PM, Salle 3052 Adrien Guatto An introduction to dependent-type checking via normalization-by-evaluation - part II Normalization-by-Evaluation (NbE) is a powerful tool often used for deciding definitional equality in dependent type theories. This talk will be a follow-up to the introduction to NbE I gave a few weeks ago. Last time, I stopped short of presenting the handling of eta laws. I will now explain how to integrate these laws into the normalizer in a type-directed way, by relying on the careful maintenance of type annotations. I will then touch upon the various ways of using the resulting normalizer to decide definitional equality and, ultimately, perform type checking of type theory. Again, my exposition will be lifted straight from _Implementing a Modal Dependent Type Theory_ by Gratzer, Sterling, and Birkedal [ICFP19]. Proofs, programs and systems Thursday April 30, 2026, 10:30AM, ENS Lyon Tba CHOCOLA seminar series Non-permanent members' seminar Thursday April 30, 2026, 4PM, Salle 3052 Manuel Catz To be announced. Graph Theory Tuesday May 5, 2026, 11AM, 3052 Tom Davot (Université d'Angers) Degreewidth: a new parameter to solve problems in tournaments We define a new parameter for tournaments called degreewidth. The degreewidth of a tournament T denoted by Delta(T) corresponds to the minimum k such that we can order the vertices of T such that every vertex is incident to at most k backward arcs, i.e. for such arcs the head is before the tail w.r.t this order. Thus, a tournament is acyclic if and only if its degreewidth is zero. Additionally, the class of sparse tournaments defined by Bessy et al. corresponds to tournaments with degreewidth one. Therefore, this parameter can be seen as a measure of how far the tournament is from being acyclic. We first study computational complexity of finding degreewidth. Namely, we show it is NP-hard and complement this result by a 3-approximation algorithm. We also provide a cubic algorithm to decide if a tournament is sparse. Finally, we study classical graph problems Dominating Set and Feedback Vertex Set parameterized by degreewidth. We show the former is fixed parameter tractable whereas the later is NP-hard on tournaments of degreewidth one. Additionally, we study Feedback Arc/Vertex Set on sparse tournaments. One world numeration seminar Tuesday May 5, 2026, 2PM, Online Gandhar Joshi (The Open University) Hiccup sequences, a Kimberling's conjecture, and Dumont-Thomas numeration systems This is part of a joint work with Robbert Fokkink (TU Delft) (https://doi.org/10.1007/s11139-025-01305-1). We generalise the self-referential sequences introduced by Benoit Cloitre in 2003 on OEIS under the umbrella term ‘hiccup sequences’ with a direct skeletal influence from a ‘remarkable’ paper by Dekking, Bosma, and Steiner (2018) describing one such sequence in five very interesting ways. In this talk, we begin with one such way that uses morphisms. Using the Dumont-Thomas numeration system (DTNS) associated with the morphism, we prove a Kimberling’s conjecture on the OEIS about the bounds of a difference sequence related to one such sequence. There is also some use of Walnut software for Ollinger provides a tool that converts the DTNS into a set of Walnut-readable automata. Enumerative and analytic combinatorics Thursday May 7, 2026, 11AM, Salle 4071 Wenjie Fang To be announced. Graph Theory Tuesday May 19, 2026, 11AM, 3052 Grégoire Beaudoire (Cnam) To be announced. Algorithms and complexity Wednesday May 20, 2026, 11AM, Salle 3052 Sampath Kannan (University of Pennsylvania) To be announced.