Welcome (original) (raw)

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.

26.3.2026
Congratulations to Geoffroy Couteau for his Amazon Research Award on his proposal on « Pseudorandom Correlations for Threshold Cryptography » (AWS Cryptography).

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).

20.3.2026
Last week, the developers of the 'uv' and 'ty' tools significantly improved their performance by using new algorithms and data structures. These tools are developed at IRIF within the Programs and Languages working group of the Proofs, Programs and Systems pôle.

'ty' is a very fast static Python typer developed by the “Astral” team, which also works on the 'uv' suite of tools, currently very prominent in the industry. It likely has hundreds of thousands of users.

Their type checking tool has data representation problems similar to those studied for “semantic subtyping”, and the discussion above (first link) shows that they implemented techniques from the thesis of Guillaume Duboc (IRIF) under the supervision of Giuseppe Castagna (IRIF), defended in January 2026; but also some of the results of the thesis by Alain Frisch, defended in… December 2004.

These changes greatly improve the performance of 'uv' on certain programs, thus giving significant visibility and a strong impact to the research conducted at IRIF.

The techniques in question were developed for the Elixir language: to learn more about this particular aspect

26.3.2026
The conference in homage to Sophie Germain on the occasion of the 250th anniversary of her birth (April 1, 1776) will take place on Monday, March 30 at 2 p.m. in the Turing Amphitheater. Program:

6.3.2026
Irif is recruiting a new financial and administrative manager (technician level). Position available from May 2026 at the earliest.

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 !

13.3.2026
IRIF will welcome M Louis Lemonnier, laureate of the FSMP's 2026 FSMP Postdocs call, as a postdoc on FSMP funds from january 1st 2027.

(These news are displayed using a randomized-priority ranking.)

Higher categories, polygraphs and homotopy
Friday April 10, 2026, 2PM, Salle 3071
Jacques Penon Pureté de la monade de Batanin

Pour montrer que l'ensemble globulaire des multi-spans est muni d'une structure d'infini-catégorie faible nous avons eu recours à une propriété particulière de la monade de Batanin : sa pureté. Au-delà de sa définition, nous allons expliquer de façon plus concrète ce que signifie cette propriété et, au passage, pourquoi l'usage de la syntaxe à guidé notre démarche.

Automata
Friday April 10, 2026, 2PM, Salle 3052
Saina Sunny (ULB) Approximate Problems for Finite Transducers

Finite state (word) transducers define rational relations and functions over words. Sequential functions are a strict subclass of rational functions recognised by input-deterministic finite state transducers. The class membership problems between those classes are known to be decidable. We consider approximate versions of these problems. This includes the approximate functionality problem, which asks whether a given rational relation is close to a rational function, and the approximate determinisation problem, which asks whether a rational function is close to a sequential function. “Close to” can be defined in different ways, by lifting standard distances between words to functions and relations. In this talk, we present the decidability results for approximate determinisation and approximate functionality problem w.r.t. Levenshtein edit distance. Also, we consider the approximate uniformisation problem, which asks, given a rational relation R, whether there exists a sequential function that is close to some function uniformising R. As its exact version, we show that this problem is undecidable.

Realizability toposes
Friday April 10, 2026, 3PM, Salle 3063
Dominik Kirst Monadic Combinatory Algebras

Formath
Monday April 13, 2026, 2PM, 3052 (+visio)
Éléonore Mangel (IRIF) Classical notions of computation and the Hasegawa-Thielecke theorem

In the spirit of the Curry-Howard correspondence between proofs and programs, we define and study a syntax and semantics for classical logic equipped with a computationally involutive negation, using a polarised effect calculus, the linear classical L-calculus. A main challenge in designing a denotational semantics for the calculus is to accommodate both call-by-value and call-by-name evaluation strategies, which leads to a failure of associativity of composition. In order to tackle this issue, we define a notion of adjunction between graph morphisms on non-associative categories, which we use to formulate polarized and non-associative notions of symmetric monoidal closed duploid and of dialogue duploid. We show that they provide a direct style counterpart to adjunction models: linear effect adjunctions for the (linear) call-by-push-value calculus and dialogue chiralities for linear continuations, respectively. In particular, we show that the syntax of the linear classical L-calculus can be interpreted in any dialogue duploid, and that it defines in fact a syntactic dialogue duploid. As an application, we establish, by semantic as well as syntactic means, the Hasegawa-Thielecke theorem, which states that the notions of central map and of thunkable map coincide in any dialogue duploid (in particular, for any double negation monad on a symmetric monoidal category).

This is joint work with Paul-André Melliès and Guillaume Munch-Maccagnoni

Graph Theory
Tuesday April 14, 2026, 11AM, 3052
Aurélie Lagoutte (G-SCOP, University Grenoble Alpes) Local certification of geometric graph classes

Local certification of a graph property is, in a sense, a distributed analogue of a nondeterministic algorithm: each vertex is given a (short) certificate, shares it with its neighbors, and must decide whether to accept it or not. The protocol is correct if all vertices accept when and only when the property holds.

In this talk, we will focus on the certificate size required to convince vertices that they belong to a graph from a certain class: (induced or not) subgraphs of the square grid, penny graphs, unit-square graphs or unit-disk graphs, 1-planar graphs, …

Most of these classes arise from geometric objects, yet they require (quasi-)linear-size certificates, unlike planar graphs for which O(log n) bits are enough.

Enumerative and analytic combinatorics
Thursday April 16, 2026, 11AM, Salle 4071
Relâche relâche

Proofs, programs and systems
Thursday April 16, 2026, 10:30AM, Salle 3052 & online (Zoom link)
Thomas Colcombet (IRIF) Finite state computations and simply typed lambda-calculus

The subject of this talk is a connection between:

- higher-order word-to-word transducers: a computation model that defines maps from words to words (more generally from terms to terms) based on simply typed lambda calculus,

- machines describing transformations from words to words: yield-Hennie machines and Ariadne transducers, and

- word-to-word mso-set-interpretations: a logical (in the sense of model theory) definition of maps from words to words.

Besides describing (some of) these objects, the emphasize of the talk will be put on the remarkable phenomenon that finite state computation models (mso-set-interpretations are of this nature) turn out to genuinely exhibit behaviors that can only (to our knowledge) be described using higher-order simple types.

This talk results from a joint work with Nathan Lhote and Pierre Ohlmann [1] in which the goal was to extend polyregular functions to an exponential growth of the output [2]. The connection between Hennie machines and higher-order transducers is from [3].

[1] *Expregular functions*. Thomas Colcombet, Nathan Lhote and Pierre Ohlmann. arXiv:2602.21019

[2] *String-to-string Interpretations with Polynomial Size Output*. Mikolaj Bojanczyk, Sandra Kiefer and Nathan Lhote. ICALP 2019: 106:1-106:14.

[3] *Tree transducers of linear size-to-height increase*. Luc Dartois, Lê Thành Dũng (Tito) Nguyễn, Charles Peyrat. Unpublished ( https://nguyentito.eu/lshi.pdf )

Non-permanent members' seminar
Thursday April 16, 2026, 4PM, Salle 3052
Slade Sanderson (IRIF) Some ergodic theory of continued fractions

Continued fractions (CFs)—which date back essentially to Euclid—possess several remarkable properties. For instance, a real number has an infinite CF expansion if and only if it is irrational (which is not true of, e.g., decimal expansions), and CFs provide the `best’ rational approximations to irrationals. In this talk, we'll survey some classical results on CFs and see how tools from ergodic theory can be used to gain new insights into these old expansions.

Automata
Friday April 17, 2026, 2PM, Salle 3052
Olivier Carton (IRIF) Mahler equations for Zeckendorf numeration

Let U = (u_n) be a Pisot numeration system. A sequence (f_n) taking values over a commutative ring R, possibly infinite, is said to be U-regularif there exists a weighted automaton which outputs f_n when it reads (n)_U. For base-q numeration, with q ∈ ℕ, q-regular sequences were introduced and studied by Allouche and Shallit, and they are a generalisation of q-automatic sequences (f_n), where f_n is the output of a deterministic automaton when it reads (n)_q. Becker, and also Dumas, made the connection between q-regular sequences, and q-Mahler typeequations. In particular a q-regular sequence gives a solution to an equation of q-Mahler type, and conversely, the solution of anisolating, or Becker, equation of q-Mahler type is q-regular.

We define generalised equations of Z-Mahler type, based on the Zeckendorf numeration system Z. We show that if a sequence over a commutative ring is Z-regular, then it is the sequence of coefficients of a series which is a solution of a Z-Mahler equation. Conversely, if the Z-Mahler equation is isolating, then its solutions define Z-regular sequences. We provide an example to show that there exist non-isolating Z-Mahler equations whose solutions do not define Z-regular sequences. Our proof yields a new construction of weighted automata that generate classical q-regular sequences.

This is joint work with Reem Yassawi.

One world numeration seminar
Tuesday April 21, 2026, 2PM, Online
Jamie Walton (University of Nottingham) To be announced.