đŹ Publications
This page is mostly in English. You will find published and unpublished documents, that are related to my research. Some of the documents are in french, and are marked as such. You will find a complete bibtex file with all the information displayed on this page. Furthermore, you can quickly cite a document using the dedicated links, that copies the appropriate LaTeX command to your clipboard.
Measuring well quasiordered finitary powersets
Preprint for (2023)
Abstract
The complexity of a wellquasiorder (wqo) can be measured through three classical ordinal invariants: the width as a measure of antichains, the height as a measure of chains, and the maximal order type as a measure of bad sequences. This article considers the âfinitary powersetâ construction: the collection Pf(X) of finite subsets of a wqo X ordered with the Hoare embedding relation remains a wqo. The width, height and maximal order type of Pf(X) cannot be expressed as a function of the invariants of X, and we provide tight upper and lower bounds for the three invariants. The article also identifies an algebra of wellbehaved wqos, that include finitary powersets as well as other more classical constructions, and for which the ordinal invariants can be computed compositionnally. This relies on a new ordinal invariant called the approximated maximal order type.

Talk at the MOVE seminar of LIS (2023)
Abstract
Regular languages over finite words are defined equivalently in terms of restrictions of Turing Machines (finite deterministic automata, and the numerous equivalent automata models that are equiexpressive in this context), syntactic presentations (regular expressions), algebraic descriptions (recognisability by finite monoids), and logical specifications (via sentences in monadic second order logic). In this talk, we propose a generalisation of regular languages, i.e.Â functions from ÎŁ* to Booleans, to functions from ÎŁ* to integers, which we call Zpolyregular functions. This class shares many similarities with regular languages, both in terms of definitions, and in terms of decidability properties. We identify Zpolyregular functions as a subclass of other existing computational models, each time with appealing characterisations. Our main result is that one can decide whether Zpolyregular functions are starfree (aperiodic), whose proof relies on two beautiful ingredients: the construction of a residual transducer, and a semantic characterisation of aperiodicity for functions that is based on multivariate polynomials. This is a joint work with GaĂ«tan DouĂ©neauTabot and Thomas Colcombet.
Compositional Techniques for Preservation Theorems over Classes of Finite Structures
Talk at the BOREAL seminar of LIRMM (2023)
Abstract
Preservation theorems connect syntactic fragments of firstorder logic to corresponding âsemanticâ properties. For instance, the fragment of unions of conjunctive queries is characterized as the fragment of (firstorder) queries that are âpreserved under homomorphismsâ, that is, if A is satisfies the query, and there is a homomorphism from A to B, then B also satisfies the query: this is known as the Homomorphism Presrevation Theorem. As an example of application of such theorems, the homomorphism preservation theorem has been used to characterize the termination of the âCore Chase Algorithmâ by Deutsch, Nash and Remmel in 2008. Preservation theorems date back to the 1950s, but the classical proofs of these result are done in the framing of Model Theory and rely heavily on the compactness theorem of first order logic. When restricting our attention to classes of finite structures (which model finite databases), the status of the preservation theorems have been investigated in the past years, with positive and negative results on different classes of finite structures, often with carefully built adhoc proofs. The goal of this talk is to recall the landscape of preservation theorems in the finite, and propose a compositional approach to constructing classes of structures over which preservation theorems can be guaranteed.
The ĆosTarski theorem and locality
Talk at the automata seminar of MIMUW (2023)
Abstract
We consider first order sentences over a finite relational signature Ï. Classical preservation theorems, dating back to the 1950s, state the correspondence between syntactic fragments of FO[Ï], and semantic ones. The archetypal example of such preservation theorem is the ĆoĆâTarski Theorem, that states the correspondence between the syntactic fragment of existential sentences, and the semantic fragment of sentences preserved under extensions. As its proof heavily relies on the compactness of first order logic, it is a priori unclear whether ĆoĆâTarski Theorem relativizes to classes of finite structures. Tait has proven in 1959 that the theorem does not relativize to the class Fin[Ï] of all finite structures, but it was proven by Atserias, Dawar, and Grohe that the ĆoĆâTarski Theorem relativizes to hereditary classes of finite structures that have bounded degree, and are closed under disjoint unions. In this talk, we provide a full characterization of classes of hereditary classes finite structures that are closed under disjoint unions for which the ĆoĆâTarski Theorem relativizes. This result follows form the study of the existentiallocal fragment of first order logic, that corresponds to a positive variant of the Gaifman normal form, and is itself subject to a preservation theorem.
\(\mathbb{Z}\)polyregular functions
Published at LICSâ23 (2023)
Abstract
This paper studies a robust class of functions from finite words to integers that we call â€polyregular functions. We show that it admits natural characterizations in terms of logics, â€rational expressions, â€rational series and transducers.We then study two subclass membership problems. First, we show that the asymptotic growth rate of a function is computable, and corresponds to the minimal number of variables required to represent it using logical formulas. Second, we show that firstorder definability of â€polyregular functions is decidable. To show the latter, we introduce an original notion of residual transducer, and provide a semantic characterization based on aperiodicity.
Fixed Points and Noetherian Topologies
Published at FoSSACSâ23 (2023)
Abstract
Noetherian spaces are a generalisation of wellquasiorderings to topologies, that can be used to prove termination of programs. They find applications in the verification of transition systems, some of which are better described using topology. The goal of this paper is to allow the systematic description of computations using inductively defined datatypes via Noetherian spaces. This is achieved through a fixed point theorem based on a topological minimal bad sequence argument.
Preservation theorems and locality of first order logic
Talk at the M2F seminar of LaBRI (2023)
Abstract
In this talk, we will investigate the tight connection between the locality properties of firstorder logic, and the relativisation (or lack thereof) of the ĆĂłsTarski Theorem to classes of structures. Starting with a gentle introduction to preservation theorems, we will then focus on two particular classes of sentences: existential formulas, and existential local formulas. We prove that existential local sentences are exactly those that can be rewritten in a positive variant of the Gaifman normal form, and can be characterized semantically as sentences that are preserved under local elementary embeddings. As expected, this semantic characterization fails in the finite. Quite surprisingly though, we can leverage this class of sentences to prove the following locality property for classes of finite structures: the ĆĂłsTarski Theorem relativises to a class C of finite structures if and only if the ĆĂłsTarski Theorem locally relativises to the class C, provided that the class C is hereditary and closed under disjoint unions. As a consequence of this result, we not only obtain new proofs of relativisation of ĆĂłsTarski Theorem, but also provide new classes where this relativisation holds.
Infinitary Noetherian Constructions II. Transfinite Words and the Regular Subword Topology
Preprint for Colloquium Mathematicum (2022)
Abstract
We show that the spaces of transfinite words, namely ordinalindexed 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.
Generic Noetherian Theorems  Defining Noetherian Topologies Through Iterations
Talk at the BRAVAS team seminar (2022)
Abstract
The goal of this talk is to provide a canonical way to construct Noetherian topologies as least fixed points. This is done by proving a least fixed point theorem, that extends the work of Hasegawa on wellquasiorderings to Noetherian spaces. This extension allows us to justify previously introduced Noetherian topologies, and construct new Noetherian spaces. Finally, note that we can apply our result to spaces that are not inductively defined, provided that the topology/ordering is inductively defined, which is a limitation in Hasegawaâs approach.
Locality and Preservation Theorems
Talk at the GT DAAL (2022)
Abstract
This talk is a brief introduction to the relationship between locality based techniques and preservation theorems in finite model theory.
Rejoindre lâadministration publique avec un doctorat  Comment et pourquoiÂ ?
Talk at the ENS ParisSaclay student seminar (2022)
Abstract
Les prĂ©sentations de lâENS dĂ©crivent souvent une formation Â« par la recherche, pour la recherche Â», selon la formule consacrĂ©e. Ainsi, une grande majoritĂ© des normaliens commencent leur parcours professionnel par un doctorat (câest le cas dâenviron 80% des Ă©lĂšves du dĂ©partement informatique). NĂ©anmoins, seuls 50% des docteurs diplĂŽmĂ©s en France rejoignent finalement les mĂ©tiers de la recherche et de lâenseignement publics. Cela contraste avec les dĂ©bouchĂ©s usuellement prĂ©sentĂ©s aux normaliens, centrĂ©s sur les postes permanents de maĂźtres de confĂ©rences, chargĂ©s de recherche ou professeurs agrĂ©gĂ©s. Parmi les docteurs, on compte Ă©galement 30% de dĂ©bouchĂ©s dans le secteur privĂ© ou lâentreprenariat. Notre objectif est de discuter des 20% restants, qui choisissent de rejoindre le secteur public hors du monde acadĂ©mique, autrement dit les administrations publiques. Les voies dâaccĂšs de la fonction publique aux jeunes docteurs sont nombreuses, quâil sâagisse de recrutements sur concours ou en tant que contractuels (CDD ou CDI), Ă des postes de managers ou dâexperts techniques. Lâobjectif de ce sĂ©minaire est de prĂ©senter les postes et les recrutements dans lâadministration, ainsi que quelques parcours de normaliens lâayant rejointe.
When Locality Meets Preservation
Published at LICSâ22 (2022)
Abstract
This paper investigates the expressiveness of a fragment of firstorder sentences in Gaifman normal form, namely the positive Boolean combinations of basic local sentences. We show that they match exactly the firstorder sentences preserved under local elementary embeddings, thus providing a new general preservation theorem and extending the ĆĂłsTarski Theorem. This full preservation result fails as usual in the finite, and we show furthermore that the naturally related decision problems are undecidable. In the more restricted case of preservation under extensions, it nevertheless yields new wellbehaved classes of finite structures: we show that preservation under extensions holds if and only if it holds locally.

Talk at the PPS Seminar at IRIF (2021)
Abstract
The âgeneric operational metatheoryâ of Johann, Simpson and VoigtlĂ€nder (LiCS 2010) defines contextual equivalence, in the presence of algebraic effects, in terms of a basic operational preorder on groundtype effect trees. We propose three general approaches to specifying such preorders: (i) operational (ii) denotational, and (iii) axiomatic; coinciding with the three major styles of program semantics. We illustrate these via a nontrivial case study: the combination of probabilistic choice with nondeterminism, for which we show that natural instantiations of the three specification methods (operational in terms of Markov decision processes, denotational using a powerdomain, and axiomatic) all determine the same canonical preorder. We do this in the case of both angelic and demonic nondeterminism.
Preservation theorems  At the crossroads of topology and logics
Talk at the ASV Seminar of IRIF (2021)
Abstract
In this talk, we introduce a family of topological spaces that captures the existence of preservation theorems. The structure of those spaces allows us to study the relativisation of preservation theorems under suitable definitions of surjective morphisms, subclasses, sums, products, topological closures, and projective limits. Throughout the talk, we also integrate already known results into this new framework and show how it captures the essence of their proofs.
Recrutement et emploi des docteurs dans les administrations publiques.
Report for IDeA (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Ă©.
Preservation Theorems Through the Lens of Topology
Published at CSLâ21 (2021)
Abstract
In this paper, we introduce a family of topological spaces that captures the existence of preservation theorems. The structure of those spaces allows us to study the relativisation of preservation theorems under suitable definitions of surjective morphisms, subclasses, sums, products, topological closures, and projective limits. Throughout the paper, we also integrate already known results into this new framework and show how it captures the essence of their proofs.
On the word topology, and beyond
BlogPost in Jean GoubaultLarrecqâs blog (2020)
Abstract
Given a quasiordered set \((X,ââ€)\), the set of finite words over \(X\) is built as \(X^*â= â_{0â\leqâkâ<â\infty} X_k\). This set can be equipped with many different quasiorders, but it appears that often the right notion is the one relying on subwords, that is, a word \(w\) is smaller than a word \(w'\) if there exists a map \(h\colonâw\tow'\) such that \(\forall 1â\leqâkâ\leqâw, w_kâ\leqâw_{h(k)}'\). This order is called the subword ordering. This blog posts explores how one can recover this ordering by looking at functions that decompose words (\(\operatorname{split} \colon X^* \to \mathcal{P}(X^* \times X^*)\)), rather than considering their inductive constructors (\(\operatorname{concat} \colon X^* \times X^* \to X^*\)).

Published at CSLâ18 (2018)
Abstract
The âgeneric operational metatheoryâ of Johann, Simpson and VoigtlĂ€nder (LiCS 2010) defines contextual equivalence, in the presence of algebraic effects, in terms of a basic operational preorder on groundtype effect trees. We propose three general approaches to specifying such preorders: (i) operational (ii) denotational, and (iii) axiomatic; coinciding with the three major styles of program semantics. We illustrate these via a nontrivial case study: the combination of probabilistic choice with nondeterminism, for which we show that natural instantiations of the three specification methods (operational in terms of Markov decision processes, denotational using a powerdomain, and axiomatic) all determine the same canonical preorder. We do this in the case of both angelic and demonic nondeterminism.
Generic Operational Metatheory
Report for ENS Cachan (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 callbyvalue 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 nondeterminism and probabilities was studied indepth.
Diagrammatic Semantics for Digital Circuits
Published at CSLâ17 (2017)
Abstract
We introduce a general diagrammatic theory of digital circuits, based on connections between monoidal categories and graph rewriting. The main achievement of the paper is conceptual, filling a foundational gap in reasoning syntactically and symbolically about a large class of digital circuits (discrete values, discrete delays, feedback). This complements the dominant approach to circuit modelling, which relies on simulation. The main advantage of our symbolic approach is the enabling of automated reasoning about parametrised circuits, with a potentially interesting new application to partial evaluation of digital circuits. Relative to the recent interest and activity in categorical and diagrammatic methods, our work makes several new contributions. The most important is establishing that categories of digital circuits are Cartesian and admit, in the presence of feedback expressive iteration axioms. The second is producing a general yet simple graphrewrite framework for reasoning about such categories in which the rewrite rules are computationally efficient, opening the way for practical applications.
A structural and nominal syntax for diagrams
Published at QPL (2017)
Abstract
The correspondence between monoidal categories and graphical languages of diagrams has been studied extensively, leading to applications in quantum computing and communication, systems theory, circuit design and more. From the categorical perspective, diagrams can be specified using (namefree) combinators which enjoy elegant equational properties. However, conventional notations for diagrammatic structures, such as hardware description languages (VHDL, Verilog) or graph languages (Dot), use a different style, which is flat, relational, and reliant on extensive use of names (labels). Such languages are not known to enjoy nice syntactic equational properties. However, since they make it relatively easy to specify (and modify) arbitrary diagrammatic structures they are more popular than the combinator style. In this paper we show how the two approaches to diagram syntax can be reconciled and unified in a way that does not change the semantics and the existing equational theory. Additionally, we give sound and complete equational theories for the combined syntax.
Une syntaxe amĂ©liorĂ©e pour la description de circuits digitaux
Report for ENS Cachan (2016)
Abstract
\(\emptyset\)