🔬 Publications
You will find published and unpublished documents, that are related to my research. Some of them are in french and will never be translated. A full list of these documents is available as a TOML file.
Preprints
Regularity as seen by Alice and Bob.
Abstract
The goal of this paper is to propose a machine-independent characterisation of functions computable by finite-state automata. Inspired by communication complexity, we introduce a model of computation that defines functions of type Σ^(*) → 𝔻, where Σ is a finite alphabet and 𝔻 is some domain. Domains of interest include: the Booleans, strings, or a field. In the model, the input string w is split into two parts w = w₁w₂, which are sent to two parties, Alice and Bob. The two parties cooperate, exchanging a constant number of messages to compute the output of the function. The messages can be either bits, or elements of the output domain. They must produce the correct output regardless of the split w = w₁w₂. For some domains, the model coincides with known finite state models: in the case of Boolean outputs it defines exactly the regular languages, and in the case of fields, it defines exactly the functions computable by weighted automata. We also conjecture that a similar situation arises for other domains, and present ample supporting evidence.Computability of Equivariant Gröbner bases.
Abstract
Let 𝕂 be a field, 𝒳 be an infinite set (of indeterminates), and 𝒢 be a group acting on 𝒳. An ideal in the polynomial ring 𝕂[𝒳] is called equivariant if it is invariant under the action of 𝒢. We show Gröbner bases for equivariant ideals are computable are hence the equivariant ideal membership is decidable when 𝒢 and 𝒳 satisfies the Hilbert’s basis property, that is, when every equivariant ideal in 𝕂[𝒳] is finitely generated. Moreover, we give a sufficient condition for the undecidability of the equivariant ideal membership problem. This condition is satisfied by the most common examples not satisfying the Hilbert’s basis property. Our results imply decidability of solvability of orbit-finite systems of linear equations and the reachability problem for reversible data Petri nets for a large class of data domains.N-polyregular functions arise from well-quasi-orderings.
Abstract
A fundamental construction in formal language theory is the Myhill-Nerode congruence on words, whose finiteness characterizes regular language. This construction was generalized to functions from finite words to ℤ by Colcombet, Douéneau-Tabot, and Lopez to characterize the class of so-called ℤ-polyregular functions. In this paper, we relax the notion of equivalence relation to quasi-ordering in order to study the class of ℕ-polyregular functions, that plays the role of ℤ-polyregular functions among functions from finite words to ℕ. The analogue of having a finite index is then being a well-quasi-ordering. This provides a canonical object to describe ℕ-polyregular functions, together with a powerful new characterization of this class.- See all of the 4 current preprints...
Conference Publications
Well-quasi-orderings on word languages.
Published at FoSSACS 2026
Abstract
The set of finite words over a well-quasi-ordered set is itself well-quasi-ordered. This seminal result by Higman is a cornerstone of the theory of well-quasi-orderings and has found numerous applications in computer science. However, this result is based on a specific choice of ordering on words, the (scattered) subword ordering. In this paper, we describe to what extent other natural orderings (prefix, suffix, and infix) on words can be used to derive Higman-like theorems. More specifically, we are interested in characterizing *languages* of words that are well-quasi-ordered under these orderings, and explore their properties and connections with other language theoretic notions. We furthermore give decision procedures when the languages are given by various computational models such as automata, context-free grammars, and automatic structures.Labelled Well Quasi Ordered Classes of Bounded Linear Clique-Width.
Published at MFCS 2025
[pdf] [slides] [bib] [arXiv] [doi]
Abstract
We construct an algorithm that inputs an MSO-interpretation from finite words to graphs, and decides if there exists a k ∈ ℕ such that the class of graphs induced by the interpretation is not well-quasi-ordered by the induced subgraph relation when vertices are freely labelled using {1, …, k}. In case no such k exists, we also prove that the class of graphs is not well-quasi-ordered by the induced subgraph relation when vertices are freely labelled using any well-quasi-ordered set of labels. As a byproduct of our analysis, we prove that for classes of bounded linear clique-width, a weak version of a conjecture by Pouzet holds.Commutative N-Rational Series of Polynomial Growth.
Published at STACS 2025
[pdf] [slides] [bib] [arXiv] [doi]
Abstract
This paper studies which functions computed by ℤ-weighted automata can be realised by ℕ-weighted automata, under two extra assumptions: commutativity (the order of letters in the input does not matter) and polynomial growth (the output of the function is bounded by a polynomial in the size of the input). We leverage this effective characterization to decide whether a function computed by a commutative ℕ-weighted automaton of polynomial growth is star-free, a notion borrowed from the theory of regular languages that has been the subject of many investigations in the context of string-to-string functions during the last decade.- See all of the 11 publications...
Journal Publications
Infinitary Noetherian Constructions II. Transfinite Words and the Regular Subword Topology.
Published at Colloquium Mathematicum
Abstract
We show that the spaces of transfinite words, namely ordinal-indexed words, over a Noetherian space, is also Noetherian, under a natural topology which we call the regular subword topology. We characterize its sobrification and its specialization ordering, and we give an upper bound on its dimension and on its stature.
Talks
2025-09-30. Polyregular Model Checking.
M2F Seminar in LaBRI. [slides]
Abstract
We reduce the model checking problem for a subset of Python to the satisfiability of a first-order formula over finite words, which is known to be decidable. The reduction is based on the theory of polyregular functions, a recently developed generalization of regular languages to polynomial output string-to-string functions. We implemented this reduction in a verification tool called PolyCheck, that can use both automata-based solvers and classical SMT solvers as backends. This is a joint work with Rafał Stefański that was pursued at the University of Warsaw, and was published at CAV'2025.2025-06-13. Polyregular Model Checking.
Automata Seminar in IRIF. [slides]
Abstract
We reduce the model checking problem for a subset of Python to the satisfiability of a first-order formula over finite words, which is known to be decidable. The reduction is based on the theory of polyregular functions, a recently developed generalization of regular languages to polynomial output string-to-string functions. We implemented this reduction in a verification tool called PolyCheck, that can use both automata-based solvers and classical SMT solvers as backends. This is a joint work with Rafał Stefański.2025-04-09. Well-Quasi-Orders and Logic on Graphs.
FMT 2025 in Les Houches. [slides]
Abstract
In this talk I will give a survey on the results and conjectures on classes of graphs that are (labelled) well-quasi-ordered by the induced subgraph relation. I will discuss how this seemingly purely combinatorial property is deeply connected to logic and structural decompositions of graphs. Starting from the early results of Ding regarding bounded tree-depth, we will explore classes of bounded clique-width, monadically stable classes, monadically dependent classes, and state various conjectures, old and new. The goal of this talk is to give an overview of the questions of interest and is targeted as a broad “Finite and algorithmic model theory” audience.- See all of the 18 talks...
Reports
Théorèmes de préservation pour la logique au premier ordre : localité, topologie et constructions limites.
PhD thesis, 2023.
[pdf] [slides] [video] [audio]
Abstract
My Ph.D ThesisRecrutement et emploi des docteurs dans les administrations publiques.
Report, 2021.
Abstract
Plus de 14 000 docteurs sont diplômés chaque année en France. À l'issue de leur thèse, ils s'intègrent au sein de trois grands secteurs : le monde académique (recherche et enseignement), le privé, ou le secteur public hors académique. Si l'insertion professionnelle dans l’académique ou le privé est régulièrement mentionnée, il semble qu’aucun rapport n’étudie l'emploi et le recrutement dans le public hors académique. Pourtant, l'Enquête emploi en continu (EEC) de l'INSEE estime à plus de 18 000 le nombre de docteurs dans ce secteur (hors doctorats de santé). L'objectif de ce rapport est donc de dresser un état des lieux de l'insertion professionnelle des docteurs au sein des administrations publiques. Il constitue une première réflexion sur un sujet peu étudié et ne prétend pas à l'exhaustivité.Generic Operational Metatheory.
Internship report, 2017.
Abstract
The goal of this internship was to give a systematic study of contextual equivalence in the presence of algebraic effects in a uniform, compact and syntactic way, in the continuation of preexisting work. To reach this objective, we extended a call-by-value PCF with a signature of algebraic effects, and gave an abstract equality between the contextual equivalence for this language and a usable logical relation, independently of the signature itself. Generic meta theorems were then proven using this abstract equivalence. To justify the usefulness of this approach, a direct link with denotational semantics and the work of Plotkin and Power was developed, and signature of mixed non-determinism and probabilities was studied in-depth.- See all of the 4 reports...