Bisimilarity, and more generally coinductive predicates, are usually presented as greatest-fixpoints. In this setting, Knaster-Tarski's fixpoint theorem corresponds to the well-known coinduction principle. For instance “to prove some processes bisimilar, find a bisimulation containing them”. By moving to Kleene iteration, and following Schäfer and Smolka, I will show how to emulate such a coinduction principle using an induction principle instead: “to prove some processes bisimilar, show that they resist to one more observation”. This principle makes it trivial to develop “up-to techniques” in a modular way ; it is also much more convenient when it comes to formalisation: it makes it possible to freely use the host language and avoids the need for guardedness checks. I will illustrate this by showing how to formalise simple examples in Rocq, using the coinduction library I developed.

Program equivalence is a central topic in the study of programming languages. Certifying that compiler transformations do not change the semantics of a program is needed to formally prove correct compilers.

This thesis aims at further developing the theory of program equivalences for the untyped pure λ-calculus, on several viewpoints.

We suggest to switch from program equivalences to program preorders, which is a usual switch in the study of programming languages but perhaps not something fully accepted at the level of the λ-calculus. We show that some central concepts in the λ-calculus may be reformulated to simple properties on preorders for λ-terms.

Contextual equivalences are the most natural notion of comparison for programs: contextual comparison is about testing programs in any execution environment and checking that they behave in a similar way. This equivalence is mostly unusable to provide proof of equivalences for expressive enough programming languages, because of the universal quantification over execution environments—akin to testing for all possible inputs.

We introduce a quantitative refinement of contextual equivalence, trying to obtain a cost-sensitive program equivalence as natural as contextual comparison. Interaction equivalence tests programs in any execution environment, checks that their behavior is similar but also takes into account the number of communications (or interactions) between the program and its environment.

Finally, we explore program equivalences for another evaluation paradigm, namely call-by-value. Call-by-value is more efficient and closer to the actual evaluation mechanism used by programming languages despite it being less studied than the original evaluation of the λ-calculus. It leads to a wide range of program equivalences, usually studied with effects added to the language. We study it here in a pure setting and show that call-by-value is a rich framework with many different notions of equivalences.

We provide a unifying view of all these program equivalences and their main properties, abstracting over the evaluation mechanisms considered.

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

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.