🔬 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 quasi-ordered finitary powersets

  Sergio AbriolaSimon HalfonAliaume LopezSylvain SchmitzPhilippe SchnoebelenIsa Vialard

  Preprint for (2023)

  [arxiv] [bib]

  Abstract

  The complexity of a well-quasi-order (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 well-behaved 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.

• Z-Polyregular functions

  Aliaume Lopez

  Talk at the MOVE seminar of LIS (2023)

  [slides] [bib]

  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 equi-expressive 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 Z-polyregular functions. This class shares many similarities with regular languages, both in terms of definitions, and in terms of decidability properties. We identify Z-polyregular functions as a subclass of other existing computational models, each time with appealing characterisations. Our main result is that one can decide whether Z-polyregular functions are star-free (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éneau-Tabot and Thomas Colcombet.

• Compositional Techniques for Preservation Theorems over Classes of Finite Structures

  Aliaume Lopez

  Talk at the BOREAL seminar of LIRMM (2023)

  [url] [slides] [bib]

  Abstract

  Preservation theorems connect syntactic fragments of first-order logic to corresponding “semantic” properties. For instance, the fragment of unions of conjunctive queries is characterized as the fragment of (first-order) 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 ad-hoc 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 Łos-Tarski theorem and locality

  Aliaume Lopez

  Talk at the automata seminar of MIMUW (2023)

  [bib]

  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 existential-local 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

  Thomas ColcombetGaëtan Douéneau-TabotAliaume Lopez

  Published at LICS’23 (2023)

  [doi] [url] [arxiv] [pdf] [slides] [video] [bib]

  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 first-order 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

  Aliaume Lopez

  Published at FoSSACS’23 (2023)

  [doi] [url] [arxiv] [pdf] [slides] [bib]

  Abstract

  Noetherian spaces are a generalisation of well-quasi-orderings 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

  Aliaume Lopez

  Talk at the M2F seminar of LaBRI (2023)

  [slides] [bib]

  Abstract

  In this talk, we will investigate the tight connection between the locality properties of first-order logic, and the relativisation (or lack thereof) of the Łós-Tarski 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 Łós-Tarski Theorem relativises to a class C of finite structures if and only if the Łós-Tarski 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 Łós-Tarski Theorem, but also provide new classes where this relativisation holds.

• Infinitary Noetherian Constructions II. Transfinite Words and the Regular Subword Topology

  Jean Goubault-LarrecqSimon HalfonAliaume Lopez

  Preprint for Colloquium Mathematicum (2022)

  [arxiv] [bib]

  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.

• Generic Noetherian Theorems - Defining Noetherian Topologies Through Iterations

  Aliaume Lopez

  Talk at the BRAVAS team seminar (2022)

  [slides] [bib]

  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 well-quasi-orderings 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

  Aliaume Lopez

  Talk at the GT DAAL (2022)

  [slides] [see] [bib]

  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 ?

  Aliaume LopezGaëtan Douéneau-Tabot

  Talk at the ENS Paris-Saclay student seminar (2022)

  [slides] [bib]

  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

  Aliaume Lopez

  Published at LICS’22 (2022)

  [doi] [url] [arxiv] [pdf] [slides] [bib]

  Abstract

  This paper investigates the expressiveness of a fragment of first-order sentences in Gaifman normal form, namely the positive Boolean combinations of basic local sentences. We show that they match exactly the first-order sentences preserved under local elementary embeddings, thus providing a new general preservation theorem and extending the Łós-Tarski 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 well-behaved classes of finite structures: we show that preservation under extensions holds if and only if it holds locally.

• Basic Operational Preorders for Algebraic Effects - With a pinch of non-determinism and probabilities

  Aliaume Lopez

  Talk at the PPS Seminar at IRIF (2021)

  [slides] [bib]

  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 ground-type 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

  Aliaume Lopez

  Talk at the ASV Seminar of IRIF (2021)

  [slides] [see] [bib]

  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.

  Gaëtan Douéneau-TabotAliaume LopezLaurent Prosperi

  Report for IDeA (2021)

  [url] [bib]

  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

  Aliaume Lopez

  Published at CSL’21 (2021)

  [doi] [arxiv] [pdf] [slides] [bib]

  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

  Jean Goubault-LarrecqAliaume Lopez

  BlogPost in Jean Goubault-Larrecq’s blog (2020)

  [url] [bib]

  Abstract

  Given a quasi-ordered 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 quasi-orders, 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|\to|w'|\) 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^*\)).

• Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular

  Aliaume LopezAlex Simpson

  Published at CSL’18 (2018)

  [doi] [url] [pdf] [slides] [bib]

  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 ground-type 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

  Aliaume Lopez

  Report for ENS Cachan (2017)

  [url] [pdf] [slides] [bib]

  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.

• Diagrammatic Semantics for Digital Circuits

  Dan R. GhicaAchim JungAliaume Lopez

  Published at CSL’17 (2017)

  [doi] [url] [arxiv] [bib]

  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 graph-rewrite 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

  Dan R. GhicaAliaume Lopez

  Published at QPL (2017)

  [doi] [url] [arxiv] [bib]

  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 (name-free) 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

  Aliaume Lopez

  Report for ENS Cachan (2016)

  [url] [pdf] [slides] [bib]

  Abstract

  \(\emptyset\)