We consider the LTL model-checking problem of concurrent self modifying code, i.e., concurrent code that has the ability to modify its own instructions during execution time. This style of code is frequently utilized by malware developers to make their malicious code hard to detect. To model such programs, we consider Self-Modifying Dynamic Pushdown Networks (SM-DPN). A SM-DPN is a network of Self-Modifying Pushdown processes, where each process has the ability to modify its current set of rules and to spawn new processes during execution time. We consider model checking SM-DPNs against single indexed LTL formulas, i.e., conjunctions of separate LTL formulas on each single process. This problem is non trivial since the number of spawned processes in a given run can be infinite. Our approach is based on computing finite automata representing the set of configurations from which the SM-DPN has a run that satisfies the single-indexed LTL formula. We implemented our techniques in a tool and obtained promising results. In particular, our tool was able to detect concurrent, self-modifying malware.

This is a joint work with Tayssir Touili.

Le droit du travail français constitue un système juridique dense, technique et en constante évolution. Il encadre des enjeux cruciaux pour la vie des salariés et des entreprises : licenciement, temps de travail, protection sociale, égalité de traitement, etc. Pourtant, malgré la centralité de ces règles dans la vie économique et sociale, leur mise en œuvre concrète reste souvent opaque, sujette à interprétation, et parfois source d’inégalités ou d’erreurs. En particulier, le calcul des indemnités de licenciement, pourtant encadré par le Code du travail et complété par les conventions collectives, repose encore sur des pratiques empiriques : simulateurs Excel hétérogènes, moteurs de règles peu transparents, ou évaluations manuelles sujettes à controverse. L’absence d’une formalisation rigoureuse et exécutable de ces règles limite à la fois la fiabilité des calculs, la transparence pour les justiciables, et l’automatisation des processus pour les professionnels du droit.

Ce projet de thèse propose de combler ce fossé en s’appuyant sur CATALA [1], un langage de programmation conçu spécifiquement pour la transcription fidèle des textes normatifs en programmes exécutables. Grâce à sa sémantique déclarative orientée juristes et à son expressivité adaptée à la logique juridique (règles, exceptions, cas particuliers), CATALA offre, en théorie, l’opportunité de rendre le droit du travail à la fois formalisé, exécutable et traçable.

Reference [1] Denis Merigoux, Nicolas Chataing, and Jonathan Protzenko. Catala : A programming language for the law. Proceedings of the ACM on Programming Languages, 5(ICFP) : 1–29, 2021a. doi : 10.1145/3473582.

The Damas-Hindley-Milner (ML) type system (used for example as the core of OCaml, SML and Haskell) is _principal_: every well-typed expression has a unique most general type. This makes inference predictable and efficient. Yet many extensions of ML (for example GADTs, higher-rank polymorphism, and static overloading) endanger principality by introducing _fragile_ constructs that resist principal inference. Existing approaches recover principality through _directional_ inference algorithms, which propagate _known_ type information in a fixed order (e.g. as in bidirectional typing) to disambiguate such constructs. However, the rigidity of a fixed inference order often causes otherwise well-typed programs to be rejected.

We propose _omnidirectional_ type inference, in which typing constraints may be solved in any order, suspending when progress requires known type information and resuming once it becomes available, using _suspended match constraints_. This approach is straightforward for simply-typed systems, but extending it to ML is challenging due to _let-generalization_. Existing ML inference algorithms type `let`-bindings `let x = e1 in e2` in a fixed order: type `e1`, generalize its type, and then type `e2`. To overcome this, we introduce _incremental instantiation_, allowing partially solved type schemes containing suspended constraints to be instantiated, with a mechanism to incrementally update instances as the scheme is refined.

It is also difficult to give a good declarative specification to this inference mechanism – the natural attempts to do this would allow “out of thin air” behavior due to causality cycles between suspended constraints. If time allows we will discuss the importance of declarative semantics for type-inference algorithms, and sketch our declarative semantics for suspended constraints.

In [1], Fiore, Plotkin and Turi develop category theoretic models for both single-variable substitution (as substitution algebras) and simultaneous substitution (as monoids for the substitution tensor) for single-sorted cartesian syntax. Since then, the literature accounts for the model of simultaneous substitution in the substructural settings of linear and affine syntax, extends it to account for multi-sorted variants, and more recently presents the theory of Superspecies to uniformly model simultaneous substitution in, for instance, the aforementioned settings and combinations thereof. In this talk, we consider models of single-variable substitution for cartesian, linear, affine and relevant syntax [2]. Crucially, this involves a modification to the uniform development of each setting — a shift from symmetric monoidal theories to (arity/coarity) monoidal theories — necessary in providing the structure to define each variation of a substitution algebra. As an application, we develop the abstract syntax of binding signatures in each of these settings and, using a generalised recursion principle, show that they are canonically equipped with the structure of a substitution algebra. In doing so, we develop machinery towards a uniform axiomatisation of single-variable substitution across substructural settings.

Joint work with Marcelo Fiore.

[1] M. Fiore, G. Plotkin and D. Turi, Abstract Syntax and Variable Binding, 14th Symposium on Logic in Computer Science (1999), 193–202. [2] M. Fiore, S. Ranchod, Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution, 40th Symposium on Logic in Computer Science (2025), 196-208.

The economy of scale principle, where the cost per unit decreases as the scale of operation increases, is a foundational concept in economics. It naturally arises in diverse real-world systems, from logistics and infrastructure planning to data summarization and information propagation. In such systems, grouping resources, demands, or actions often leads to more efficient outcomes. This behavior is reflected in mathematical models through properties such as submodularity, which captures diminishing returns on the value side, and subadditive capacity cost functions, which formalize buy-at-bulk effects on the cost side. In submodular optimization problems, the economy of scale appears as diminishing marginal gains: each additional element contributes less marginal gain as the solution grows. This framework captures key phenomena, including information redundancy and influence propagation. In the buy-at-bulk facility location problem, the economy of scale manifests on the cost side: satisfying a larger demand becomes cheaper per unit due to amortized setup costs. By leveraging this shared structure, this thesis explores the design of approximation and streaming algorithms for these two classes of problems that capture the principle of economy of scale. We develop algorithmic techniques with provable performance guarantees for problems with complex constraints, across different computational models. These results contribute to the broader understanding of scalable algorithms for decision making tasks where gains or costs exhibit diminishing return structures.

We consider two related problems. The transition to chaos in the sense of positive topological entropy for one-dimensional piecewise smooth maps, and the transition to positive Hausdorff dimension for the survivor set of associated open maps. We describe an iterative process that determines the boundaries of positive topological entropy (resp. positive Hausdorff dimension). The boundary can then be characterised via substitution sequences that generalise the Thue-Morse sequence for continuous maps of the interval. This work is joint with Clément Hege.

Geometry lies at the heart of optimization, where the seemingly simple decision of “to choose or not to choose an object” often uncovers profound insights into the structure and solutions of complex problems. This geometric perspective has wide-ranging applications across various fields, including machine learning, logistics, computer graphics, sensor networks, and many others. In this talk, I will focus on two fundamental aspects of geometric optimization problems: Packing and Independence.

Consider a set of D-dimensional objects (each with associated profits), and the goal is to find the maximum-profit subset that can be packed without overlap into a given D-dimensional hypercube. This problem is known as the Geometric Knapsack Problem. The packing of various kinds of objects has been extensively studied in mathematics over the centuries. Interestingly, the problem becomes computationally intractable even in rather simple settings, e.g., unit disks in 2D. In this talk, I will present a polynomial-time approximation scheme for packing D-dimensional balls.

On the other hand, the Independent Set problem for a set of objects in D-dimensional space aims to find a maximum-cardinality subset of independent (i.e., pairwise-disjoint) objects. Independent Set is one of the most fundamental problems in theoretical computer science, and unfortunately, it is known to be inapproximable in the most general cases. There has been extensive research on polynomial-time algorithms with improved approximation ratios for geometric inputs, sometimes trading off efficiency in running times. In this talk, I will present near-linear-time constant-factor approximation algorithms for various natural families of objects, e.g., balls, boxes, fat objects, etc.

See https://chocola.ens-lyon.fr/events/seminaire-2025-11-13/

The use of rewriting-based visual formalisms is on the rise. In the formal methods community, this is partly due to the introduction of adhesive categories, where most properties of classical approaches to graph transformation, such as those on parallelism and confluence, can be rephrased and proved in a general and uniform way. E-graphs (EGGs) are a formalism for program optimisation via an efficient implementation of equality saturation. In short, EGGs are (acyclic) term graphs with an additional equivalence on nodes that is closed under the operators of the signature. Instead of replacing the components of a program, the optimisation step adds new components and links them to the existing ones via an equivalence relation, until an optimal program is reached. This work describes EGGs via adhesive categories. Besides the benefits in itself of a formal presentation, which renders the properties of the data structure precise, the description of the addition of equivalent program components using standard graph transformation tools offers the advantages of the adhesive framework in modelling, for example, concurrent updates.