Le calendrier des séances (format iCal).
Pour ajouter le calendrier des séances à votre agenda favori, souscrire au calendrier en indiquant ce lien.

Séances passées

Année 2021

Soutenances de thèses
Mercredi 7 juillet 2021, 14 heures, Salle 3052 et Zoom
Yassine Hamoudi (IRIF) Quantum Algorithms for the Monte Carlo Method

The Monte Carlo method is a central paradigm of algorithm design that consists of using statistical analysis and random sampling to solve problems that have a probabilistic interpretation. This thesis explores the advantages offered by a quantum computer to speed up this method in three directions. First, we consider the problem of estimating average values in a time-efficient way. Secondly, we study the task of importance sampling and its applications to stochastic optimization. Finally, we examine the power of quantum algorithms that operate with limited memory.


Soutenances de thèses
Mardi 29 juin 2021, 10 heures, Amphithéâtre Alan Turing & Zoom
Rémi Nollet (IRIF) A study of circular representations of infinite proofs for fixed-points logics, their5expressiveness and complexity.

Soutenances de thèses
Mardi 11 mai 2021, 15 heures, Online
Yixin Shen (IRIF) Classical and quantum cryptanalysis for Euclidean lattices and subset sum

Post-quantum cryptography is a branch of cryptography that aims at designing non-quantum (i.e. classical) cryptographic systems, which are protected against an adversary possessing a quantum computer. In this thesis, we focus on the study of two fundamental problems for post-quantum cryptography: the shortest vector problem (SVP) and the random subset sum problem. We propose several classical/quantum algorithms that improve the state of the art.

Soutenances de thèses
Mardi 30 mars 2021, 16 heures, Online
Nicolas Jeannerod (IRIF) Verification of Shell Scripts Performing File Hierarchy Transformations

This thesis aims at applying techniques from deductive program verification and analysis of tree transformations to the problem of analysing Shell scripts. In particular, we aim at analysing Shell scripts that are used in software installation in the Debian GNU/Linux distribution. The final goal is to build a proof-of-concept tool able to read Debian packages – the way Debian has to distribute software – and report on their quality and on the potential bugs they might have.

Shell is a scripting language providing control structures around Unix utility calls. Unix utilities are objects that can perform all kind of transformation on Unix filesystems. We model Unix filesystems using feature trees and transformations of Unix filesystems using formulas in a feature tree logic named FTS. We describe these modelisations extensively and discuss their validity. The control structures of Shell scripts are converted to control structures in an intermediary language that has clearly defined semantics. This involves the definition of this intermediary language, the design of a static parser for Shell scripts and of a conversion that respects the semantics of both languages. The semantics of Shell scripts is then computed using symbolic execution of the aforementioned intermediary language, using a database of specifications of Unix utility calls as formulas of FTS. The result is, for each potential trace of execution of a Shell script, a formula of FTS describing the filesystem transformation this trace performs.

The main part of the thesis then focuses on decidability of formulas of FTS. The goal is to be able to detect traces of execution of Shell scripts that cannot happen and to check properties on the Shell scripts, such as “if the script fails, then it must not have performed any transformation”. A first, theoretical, part aims at showing that the full first-order theory of FTS is decidable. This goes by first reasoning only on Σ₁-formulas of FTS and defining a system of rules R₁ that transforms Σ₁-formulas. We show that we can use R₁ to decide the satisfiability of Σ₁-formulas as well as some other properties. We then extend the reasoning from Σ₁-formulas to first-order formulas of FTS using properties of R₁ and weak quantifier eliminations. We conclude by stating that the first-order theory of FTS is indeed decidable. A second, more practical, part aims at designing efficient decision procedures for a subset of FTS rich enough to express the semantics of Unix utilities and Shell scripts. This goes by focusing on conjunctive formulas and improving on R₁. This results in a system R₂ which is more efficient on conjunctive formulas but would not have the required properties to prove decidability of the first-order. We then show how R₂ can be implemented efficiently and that it can be extended without loss of efficiency to support specific forms of Σ₁-formulas.

Finally, this thesis describes the applications of the theoretical work to the implementation of a toolchain able to analyse all software packages in the Debian distribution and report on them. We describe our analysis and the bugs that we have found during the whole project. This thesis takes place within the CoLiS project, ANR-15-CE25-0001, taking place from October 2015 to March 2021.

Soutenances de thèses
Mardi 30 mars 2021, 9 heures 30, Online
Ranadeep Biswas (IRIF) Automated Formal Testing of Storage Systems and Applications

As internet grows to be cheaper and faster, distributed software systems and applications are becoming more and more ubiquitous. Today they are the backbone of a large number of online services like banking, e-commerce, social networking, etc. As the popularity of these softwares increases, it is very important that they ensure strong levels of reliability and security.

Modern distributed software is centered around using large-scale storage systems for storing and retrieving data. To ensure persistence and availability of data in the presence of failures, these systems maintain data in multiple copies that are stored on different nodes in the network. Then, for performance reasons, these copies are allowed to (temporarily) diverge, an instance of the so-called weak-consistency, which makes the semantics of concurrent accesses to data quite complex.

Over the recent years, many solutions for implementing weakly-consistent storage systems have been proposed. These implementations are most often very complex and error-prone. The specific levels of weak consistency they ensure are most often described only informally, which makes it difficult to reason about them. Moreover, in many cases, there are significant discrepancies between the guarantees claimed in their documentation and the guarantees that they really provide.

The objective of this dissertation is to propose algorithmic techniques for automated testing of weakly-consistent distributed systems against formal specifications. We focus on an important class of distributed data types, called Conflict-Free Replicated Data Types (CRDTs for short), that include many variations like registers, flags, sets, arrays, etc., and on Transactional Systems (Databases), which enable computations on shared data that are isolated from other concurrent computations and resilient to failures. We introduce formal specifications for such systems and investigate the asymptotic complexity of checking whether a given execution conforms to such specifications. We also study the problem of testing applications that run on top of weakly-consistent transactional systems, introducing a mock in-memory storage system that simulates the behaviors of such systems according to their formal specifications.

Soutenances de thèses
Lundi 15 mars 2021, 14 heures 30, Online
Sidi Mohamed Beillahi (IRIF) Automated Verification of Programs Running on top of Distributed Systems

Over the past decades, distributed software became an integral part of our society, being used in various domains like online banking or shopping, distance learning, supply chain, and telecommuting. Developing correct and efficient distributed systems is a major and timely challenge. The objective of this dissertation is to propose algorithmic techniques for improving the reliability of such software, focusing on applications ran on top of distributed storage systems like databases and blockchain. Databases allow applications to access data concurrently from multiple sites in a network. Blockchain is a cryptographically-secure distributed ledger that allows to perform irreversible actions between different parties without a trusted authority.

The effect of a set of database transactions executing in parallel is specified using a formalism called consistency model. For instance, serializability states that a set of transactions behave as if they were executed serially one after another even if they actually overlap in time. Although simple to understand, serializability carries a significant penalty on performance and modern databases implement weaker consistency models. In general, these weak models are more complex to reason about. In this dissertation, we investigate the problem of checking a property of applications called robustness. Given two comparable consistency models, an application is called robust if it has the same behaviors when ran on top of databases implementing these two models. This dissertation investigates the theoretical complexity of checking robustness in the context of several consistency models: causal consistency, prefix consistency, snapshot isolation, and serializability. It provides non-trivial reductions to a well-studied problem in formal verification, assertion checking, that enables the reuse of existing verification technology. Besides theoretical results, it proposes pragmatic approaches based on under/over-approximations that are evaluated on practical applications.

Applications ran on top of blockchain are deployed in the form of smart contracts that manipulate the blockchain state. Smart contracts are mainly used to govern trading in cryptoassets that are worth billions of US dollars, and bugs can lead to huge financial losses. Exacerbating the impact of these bugs is the fact that smart contracts cannot be modified once they are deployed on the blockchain. Applying techniques from formal verification to audit smart contracts can help in avoiding expensive bugs. However, since most smart contracts are not annotated with formal specifications, formal verification of functional properties is impeded. To overcome this problem, this dissertation investigates notions of refinement between smart contracts, which enable the re-use of verified contracts as specifications for other contracts, thus scaling up the overall verification effort.

Soutenances de thèses
Jeudi 28 janvier 2021, 15 heures, Online
Léonard Guetta (IRIF) Homology of strict omega-categories

The objective of this thesis is to compare the homology of the nerve of an ω-category, invariant coming from the homotopy theory of strict ω-categories, with its polygraphic homology, invariant coming from higher rewriting theory. More precisely, we prove that both homologies generally do not coincide and call homologically coherent the particular strict ω-categories for which polygraphic homology and homology of the nerve do coincide. The goal pursued is to find abstract and concrete criteria to detect homologically coherent ω-categories.

Soutenances de thèses
Vendredi 8 janvier 2021, 9 heures 30, Online
Simon Forest (IRIF) Computational Description of Higher Categories

Higher categories are algebraic structures consisting of cells of various dimensions equipped with notions of composition, which have found many applications in mathematics (algebraic topology in particular) and theoretical computer science. They are notably complicated structures whose manipulation is technical and error-prone. The purpose of this thesis is to introduce several computational tools for strict and semi-strict variants of higher categories that ease the study of these objects. In order to represent higher categories as finite data, so that they can be given as input to a program, we use the structure of polygraph, initially introduced by Street and Burroni for strict categories and then generalized by Batanin to any algebraic theory of higher category, which allows presenting higher categories by means of systems of generators. The first problem tackled by this thesis is then the one of the word problem on strict categories, which consists in deciding whether two formal composites of cells of strict categories represent the same cell. We give an implementable and relatively efficient solution for it by improving the decidability procedure initially given by Makkai. Then, we turn to pasting diagram formalisms for strict categories, which enable to efficiently represent cells of strict categories using set-like structures and for which a reliable implementation is desirable. We consider the three main formalisms which have been introduced until now, namely Street's parity complexes, Johnson's pasting schemes and Steiner's augmented directed complexes. Our study reveals that the axiomatics of the first two ones are defective, which motivates the introduction of a new structure, called torsion-free complexes, whose axioms have nice properties and generalize those of the three other formalisms. We also show that they are amenable to concrete computation, by providing an implementation of those. Finally, we consider the problem of coherence of presentations of algebraic structures expressed in 3-dimensional weak categories, the latter being known to be equivalent to Gray categories. Taking inspiration from a celebrated result given by Squier in the context of monoids, we adapt the classical tools from rewriting theory to the setting of Gray categories and relate the coherence of presentations of Gray categories to the confluence of the critical branchings of an associated rewriting system. From this result, we deduce a semi-automated procedure to find coherent presentations of Gray categories that we apply on several examples.

Année 2020

Soutenances de thèses
Vendredi 4 décembre 2020, 14 heures, Online
Isaac Konan (IRIF) Rogers-Ramanujan type identities: bijective proofs and Lie-theoretic approach

The topic of this thesis belongs to the theory of integer partitions, at the intersection of combinatorics and number theory. In particular, we study Rogers-Ramanujan type identities in the framework of the method of weighted words. This method revisited allows us to introduce new combinatorial objects beyond the classical notion of integer partitions: the generalized colored partitions. Using these combinatorial objects, we establish new Rogers-Ramanujan identities via two different approaches. The first approach consists of a combinatorial proof, essentially bijective, of the studied identities. This approach allowed us to establish some identities generalizing many important identities of the theory of integer partitions: Schur’s identity and Göllnitz’ identity, Glaisher’s identity generalizing Euler’s identity, the identities of Siladi´c, of Primc and of Capparelli coming from the representation theory of affine Lie algebras. The second approach uses the theory of perfect crystals, coming from the representation theory of affine Lie algebras. We view the characters of standard representations as some identities on the generalized colored partitions. In particular, this approach allows us to establish simple formulas for the characters of all the level one standard representations of type A_{n-1}^{(1)},A_{2n}^{(2)},D_{n+1}^{(2)},A_{2n-1}^{(2)},B_{n}^{(1)},D_{n}^{(1)}.

Soutenances de thèses
Jeudi 26 novembre 2020, 13 heures, Online
Alexandre Nolin (IRIF) Communication complexity: large output functions, partition bounds, and quantum nonlocality

Most classical problems of communication complexity are Boolean functions. When considering functions of larger output, the way in which the result of a computation must be made available – the output model – can greatly impact the complexity of the problem. In particular, some lower bounds may not apply to all models. In this thesis, we study some lower bounds affected by the output model, problems with large outputs, revisit several classical results in the light of these output mechanisms, and relate them to the formalism of behaviors and Bell inequalities of quantum nonlocality.

Soutenances de thèses
Lundi 23 novembre 2020, 10 heures, Remote
Alessandro Luongo (IRIF) Quantum algorithms for machine learning

Cette thèse présente de nouveaux algorithmes quantiques pour l'apprentissage automatique. L'ordinateur quantique permet un nouveau paradigme de calcul qui exploite les lois de la mécanique quantique pour offrir une accélération des calculs par rapport aux ordinateurs classiques.Dans cette thèse, je propose des algorithmes quantiques pour l'apprentissage de certains modèles d'apprentissage classique. Les nouveaux algorithmes quantiques développés ont été implémentés et simulés sur des ordinateurs classiques à base d’HPC, avec les jeux de donnés couramment utilisés pour l’apprentissage automatique classique. Je démontre ainsi que ces algorithmes ont effectivement le potentiel de concourir contre les meilleurs algorithmes classiques pour l’analyse de donnés.

Soutenances de thèses
Mercredi 4 novembre 2020, 15 heures, Online
Brieuc Guinard (IRIF) Intermittent Lévy Walks and their applications in biological searches

Throughout the last two decades, a type of trajectories has been found to be almost ubiquitous in biological searches: the Lévy Patterns. Such patterns are fractal, with searches happening in self-similar clusters. Their hallmark is that their step-lengths are distributed in a power-law with some exponent μ ∈ (1, 3). This discovery lead to two intriguing questions: first, do these patterns emerge from an internal mechanism of the searcher, or from the interaction with the environment? Second, and independently of the previous question: what do these searchers have in common? When can we expect to see a Lévy Pattern of exponent μ? And how much does the knowledge of μ inform on the biological situation? Towards answering this second question, I will present an analysis of the efficiency of Lévy Walks when detection is weak, and targets appear in various sizes. In particular, I show that the much-debated inverse-square Lévy Walk is uniquely efficient in this setting. Regarding the question of how animals can perform Lévy Patterns, it has been suggested that animals could approximate a Lévy distribution by having k different modes of movement, where k = 2, 3. I will provide tight bounds for the performances of such an algorithm, which show, in accordance with the literature, that having k = 3 modes may be sufficiently efficient in biological scenarios.

Soutenances de thèses
Jeudi 15 octobre 2020, 16 heures, Online
Cédric Ho Thanh (IRIF) Opetopes: Syntactic and Algebraic Aspects

Opetopes are shapes (akin to globules, cubes, simplices, dendrices, etc.) introduced by Baez and Dolan to describe laws and coherence cells in higher-dimensional categories. In a nutshell, they are trees of trees of trees of trees of… These shapes are attractive because of their simple nature and easy to find “in nature”, but their highly inductive definition makes them difficult to manipulate efficiently.
This thesis develops the theory of opetopes along three main axes. First, we give it clean and robust foundations by carefully detailing the approach of Kock et. al., based on polynomial monads and trees. Then, with the aim of computerized manipulation in mind, we introduce two syntactical approaches to opetopes and opetopic sets. In each, opetopes are represented as syntactical constructs whose well-formation conditions are enforced by corresponding sequent calculi. Lastly, we focus on the algebraic structures that can naturally be described by opetopes. So-called opetopic algebras include categories, planar operads, and Loday's combinads over planar trees. We show how classical results of Rezk, Joyal and Tierney (for ∞-categories), and Cisinski and Moerdijk (for ∞-operads) can be reformulated and generalized in the opetopic setting.


Soutenances de thèses
Vendredi 26 juin 2020, 14 heures, Online
Baptiste Louf (IRIF) Cartes de grand genre : de la hiérarchie KP aux limites probabilistes

Cette thèse s’intéresse aux cartes combinatoires, qui sont définies comme des plongements de graphes sur des surfaces, ou de manière équivalente comme des recollements de polygones. Le genre g de la carte est défini comme le nombre d’anses que possède la surface sur laquelle elle est plongée. En plus d’être des objets combinatoires, les cartes peuvent être représentées comme des factorisations de permutations, ce qui en fait également des objets algébriques, qu’on peut notamment étudier grâce à la théorie des représentations du groupe symétrique. En particulier, ces propriétés algébriques des cartes font que leur série génératrice satisfait la hiérarchie KP( et sa généralisation, la hiérarchie 2-Toda). La hiérarchie KP est un ensemble infini d’équations aux dérivées partielles en une infinité de variables. Les équations aux dérivées partielles de la hiérarchie KP se traduisent ensuite en formules de récurrence qui permettent d’énumérer les cartes en tout genre. D’autre part, il est intéressant d’étudier les propriétés géométriques des cartes, et en particulier des très grandes cartes aléatoires. De nombreux travaux ont permis d’étudier les propriétés géométriques des cartes planaires, c’est à dire de genre 0. Dans cette thèse, on étudie les cartes de grand genre, c’est à dire dont le genre tend vers l’infini en même temps que la taille de la carte. Ce qui nous intéressera particulièrement est la notion de limite locale, qui décrit la loi du voisinage d’un point particulier (la racine) des grandes cartes aléatoires uniformes. La première partie de cette thèse est une introduction à toutes les notions nécessaires : les cartes, bien entendu, mais également la hiérarchie KP et les limites locales. Dans un deuxième temps, on cherchera à approfondir la relation entre cartes et hiérarchie KP, soit en expliquant des formules existantes par des constructions combinatoires, soit en découvrant de nouvelles formules. La troisième partie se concentre sur l’étude des limites locales des cartes de grand genre, en s’aidant notamment de résultats obtenus grâce à la hiérarchie KP. Enfin, on conclut par quelques problèmes ouverts.


Année 2019

Soutenances de thèses
Mardi 17 décembre 2019, 10 heures, Salle 0010, Bâtiment Sophie Germain
Mengchuan Zou (IRIF) Aspects of Efficiency in Selected Problems of Computation on Large Graphs

This thesis presents three works on different aspects of efficiency of algorithm design for large scale graph computations.

In the first work, we consider a setting of classical centralized computing, and we consider the question of generalizing modular decompositions and designing time-efficient algorithm for this problem. Modular decomposition, and more broadly module detection, are ways to reveal and analyze modular properties in structured data. As the classical modular decomposition is well studied and have an optimal linear-time algorithm, we firstly study the generalizations of these concepts to hypergraphs and present here positive results obtained for three definitions of modular decomposition in hypergraphs from the literature. We also consider the generalization of allowing errors in classical graph modules and present negative results for two this kind of definitions.

The second work focuses on graph data query scenarios. Here the model differs from classical computing scenarios in that we are not designing algorithms to solve an original problem, but we assume that there is an oracle which provides partial information about the solution to the original problem, where oracle queries have time or resource consumption, which we model as costs, and we need to have an algorithm deciding how to efficiently query the oracle to get the exact solution to the original problem, thus here the efficiency is addressing to the query costs. We study the generalized binary search problem for which we compute an efficient query strategy to find a hidden target in graphs. We present the results of our work on approximating the optimal strategy of generalized binary search on weighted trees.

Our third work draws attention to the question of memory efficiency. The setup in which we perform our computations is distributed and memory-restricted. Specif- ically, every node stores its local data, exchanging data by message passing, and is able to proceed local computations. This is similar to the LOCAL/CONGEST model in distributed computing, but our model additionally requires that every node can only store a constant number of variables w.r.t. its degree. This model can also describe natural algorithms. We implement an existing procedure of multiplicative reweighting for approximating the maximum s–t flow problem on this model, this type of methodology may potentially provide new opportunities for the field of local or natural algorithms.

From a methodological point of view, the three types of efficiency concerns cor respond to the following types of scenarios: the first one is the most classical one – given the problem, we try to design by hand the more efficient algorithm; the second one, the efficiency is regarded as an objective function – where we model query costs as an objective function, and using approximation algorithm techniques to get a good design of efficient strategy; the third one, the efficiency is in fact posed as a constraint of memory and we design algorithm under this constraint.

Soutenances de thèses
Lundi 16 décembre 2019, 14 heures 30, Salle 2017, Bâtiment Sophie Germain
Adrien Husson (IRIF) Logical foundations of a modelling assistant for molecular biology

This thesis addresses the issue of “Executable Knowledge Representation” in the context of molecular biology. We introduce the foundation of a logical framework, termed iota, whose aim is to facilitate knowledge collation of molecular interactions at the level of proteins and at the same time allows the modeler to compile a reasonable fragment of the logic into a finite set of executable graph rewriting rules. We define a logic FO[↓] over cell state transitions. States represent cell contents; domain elements are protein parts and relations are protein-protein bindings. The unary logical operator ↓ selects transitions where as little as possible happens. Formulas over transitions also may runs, which are finite or infinite sequences of transitions. Every transition formula is also associated to a set of rewriting rules equipped with an operational semantics. We introduce two deductive systems that act as “typing” for formulas. We show that if a formula is typable in the first system then the execution of its associated rule set produces exactly the runs denoted by the formula, and that if it is typable in the second system then its associated rule set is finite. We introduce a grammar that produces formulas typable in both systems, up to logical equivalence. Finally we study decidability and definability properties of fragments of FO[↓]. In particular, we show that formulas typable in the second system are in a tight fragment of FO, which implies that the operator ↓ can then be eliminated.


Soutenances de thèses
Jeudi 12 décembre 2019, 14 heures, Salle 2014, Bâtiment Sophie Germain
Théo Zimmermann (IRIF) Challenges in the collaborative evolution of a proof language and its ecosystem

In this thesis, I present the application of software engineering methods and knowledge to the development, maintenance, and evolution of Coq —an interactive proof assistant based on type theory— and its package ecosystem. Coq has been developed at Inria since 1984, but has only more recently seen a surge in its user base, which leads to much stronger concerns about its maintainability, and the involvement of external contributors in the evolution of both Coq, and its ecosystem of plugins and libraries.

Recent years have seen important changes in the development processes of Coq, of which I have been a witness and an actor (adoption of GitHub as a development platform, first for its pull request mechanism, then for its bug tracker, adoption of continuous integration, switch to shorter release cycles, increased involvement of external contributors in the open source development and maintenance process). The contributions of this thesis include a historical description of these changes, the refinement of existing processes, and the design of new ones, the design and implementation of new tools to help the application of these processes, and the validation of these changes through rigorous empirical evaluation.

Involving external contributors is also very useful at the level of the package ecosystem. This thesis additionally contains an analysis of package distribution methods, and a focus on the problem of the long-term maintenance of single-maintainer packages.


Soutenances de thèses
Lundi 9 décembre 2019, 14 heures, Salle 3052, Bâtiment Sophie Germain
Simon Collet (IRIF) Algorithmic Game Theory Applied to Networks and Populations

The aim of this thesis is to use algorithmic game theory tools to study various games inspired from real world problems in the fields of information networks and biology. These games are characterized by a large number of players, each with incomplete information about other players. In classical game theory, these games fall into the category of extensive games with imperfect information, which are modeled using trees. However, these games remain very difficult to analyze in details, because of their intrinsic complexity, which is linked with their possibly infinite tree depth. Nevertheless, we have taken up the challenge of this task, while diversifying the methods of resolution, and emphasizing its interdisciplinary aspect.

Besides the introduction and the conclusion, the thesis is divided into three parts. In the first part, we adopt the point of view of classical game theory. We propose a game that corresponds to a wide class of problems encountered in the theory of distributed computing. The main contributions of this part are, on the one hand, to show how to transform a purely algorithmic problem into a game, and, on the other hand, to prove the existence of satisfactory equilibria for the resulting class of games. This second point is essential, as it guarantees that game theory is adapted to the study of distributed games, despite their complexity.

The second part is dedicated to the study of a game omnipresent within biological systems, that we call dispersion game. This game models the situation in which a group of animals must share a certain amount of resources scattered among different geographical sites. The difficulty of the game comes from the fact that some sites contain more resources than others, but may also attract more players. We propose a rule for the distribution of resources which makes it possible to maximize the resources exploited by the whole group. This part of the thesis is also an opportunity to revisit the close links between the concept of ideal free distribution, very present in the theory of foraging, and the concept of evolutionarily stable strategy, a key concept of evolutionary game theory.

The third part focuses on the study of the behavior of a specific species of small bats living in Mexico, in the Sonoran Desert, and feeding at night from the nectar of the giant Saguaro cacti, a protected species. After the presentation of the experimental results obtained in the field, we propose a computer simulation of their behavior. The results of these simulations make it possible to formulate interesting hypotheses about the cerebral activities of these small mammals. We then study a theoretical model of game inspired by this real situation. The study of this abstract model allows us to distinguish the fundamental characteristics of the game, and to reinforce our approach of theorizing foraging behavior. This study also opens the way to applying this type of model to other situations, involving animal or human behavior.

Soutenances de thèses
Vendredi 6 décembre 2019, 15 heures 30, Salle 1009, Bâtiment Sophie Germain
Jules Chouquet (IRIF) Une Géométrie du calcul : Réseaux de preuve, Appel-Par-Pousse-Valeur et topologie du Consensus

Cette thèse propose une étude quantitative de plusieurs modèles de calcul de l’informatique fondamentale et de la théorie de la démonstration. Deux approches sont menées : la première consiste à examiner les mécanismes d’approximation multilinéaires dans des systèmes issus du λ-calcul et de la Logique Linéaire. La seconde consiste à étudier les modèles topologiques pour les systèmes distribués et à les adapter aux algorithmes probabilistes.

On étudie d’abord le développement de Taylor des réseaux de preuve de la Logique Linéaire. On introduit des méthodes de démonstration qui utilisent la géométrie de l’élimination des coupures des réseaux multiplicatifs, et qui permettent de manipuler des sommes infinies de réseaux de façon sûre et correcte, pour en extraire des propriétés sur les réductions qui sont à l’œuvre.

Ensuite, nous introduisons un langage permettant de définir le développement de Taylor syntaxique pour l’Appel-Par-Pousse-Valeur (Call-By-Push-Value), en capturant certaines propriétés de la sémantique dénotationelle liées aux morphismes de coalgèbres.

Puis nous nous intéressons aux systèmes distribués (à mémoire partagée, tolérants aux pannes), et au problème du Consensus. On utilise un modèle topologique qui permet d’interpréter la communication dans les complexes simpliciaux, et on l’adapte de façon à transformer les résultats d’impossibilité bien connus en résultats de borne inférieure de probabilité pour des algorithmes probabilistes.

English version:

This Phd thesis presents a quantitative study of various computation models of fundamental computer science and proof theory, in two principad directions: the first consists in the examination of mecanismis of multilinear approximations in systems related to λ-calculus and Linear Logic. The second consists in a study of topological models for asynchronous distributed systems, and probabilistic algorithms.

We first study Taylor expansion in Linear Logic proof nets. We introduce proof methods using the geometry of cut elimination in multiplicative nets, and which allow to work with infinite sums of nets in a safe and correct way, in order to extract properties about reduction.

Then, we introduce a language allowing us to define Taylor expansion for Call-By-Push-Value, while capturing some properties of the denotational semantics, related to coalgebras morphisms.

We focus then on fault tolerant-distributed systems with shared memory, and to Consensus problem. We use a topological model which allows to interpret communication with simplicial complexes, and we adapt in so as to transform the well-known impossibility results in lower bounds for probabilistic algorithms.

Manuscript: https://www.irif.fr/~chouquet/these.html

Soutenances de thèses
Mardi 3 décembre 2019, 14 heures 30, Salle 3052, Bâtiment Sophie Germain
Clément Jacq (IRIF) Categorical Combinatorics for Non-Deterministic Innocent Strategies

Twenty-five years ago, Hyland and Ong resolved the full abstraction problem for the PCF language by constructing a game semantics based on the fundamental notion of innocent strategy. We carry on their work in this thesis, and construct a 2-dimensional category of non-deterministic and innocent strategies extending their original deterministic innocent game model.

Our starting point in the thesis is provided by the combinatorial approach to innocent strategies developed by Harmer, Hyland and Melliès in a work published ten years ago. In this work, they elaborate a combinatorial description of the pointer structures of arena games, and establish that innocence can be recovered by taking advantage of a number of remarkable categorical properties, most notably the existence of a distributive law between the monad generating the Player views and the comonad generating the Opponent views.

In this thesis, we study in great detail the reconstruction of the innocent game model identified by Harmer, Hyland and Melliès, and extend this model in two directions. In the first direction, we explain how to see the Harmer-Hyland-Melliès game model as a specific instance of a dialogue category, a notion originally introduced by Melliès, using the underlying symmetry between Opponent and Player in categories of games and strategies.

In the second direction, we construct a 2-dimensional game semantics of non-deterministic PCF by equipping every game with a presheaf of non-deterministic strategies, instead of just a set of strategies. In order to perform this shift of dimension from sets to presheaves, we adapt very carefully the categorical constructions involved in the Harmer-Hyland-Melliès model, and construct in particular a pseudo-distributive law between the pseudo-monad generating the Player views and the pseudo-comonad generating the Opponent views in our non-determinic game model. We obtain in this way a bicategory of games, non-deterministic innocent strategies and simulations — which we then compare with alternative formulations of non-deterministic and innocent game semantics appearing in the literature.

Soutenances de thèses
Vendredi 21 juin 2019, 15 heures, Amphithéâtre Turing
Nikola K. Blanchard (IRIF) Usability: low tech, high security

Soutenances de thèses
Jeudi 20 juin 2019, 14 heures 30, Salle 0011
Raphaëlle Crubillé (IRIF) Behavioural distances for higher-order probabilistic programs

The manuscript is available at: http://research.crubille.lautre.net/main.pdf

Année 2018

Soutenances de thèses
Vendredi 7 décembre 2018, 14 heures, Salle François Jacob, bâtiment Buffon
Pierre Cagne (IRIF) Towards a homotopical algebra of dependent types

Soutenances de thèses
Vendredi 30 novembre 2018, 14 heures 30, Salle 580F, Bâtiment Halle aux Farines
Lucas Boczkowski (IRIF) Search and Broadcast in Stochastic Environments, a Biological Perspective

This thesis is built around two series of works, each motivated by experiments on ants. We derive and analyse new models that use computer science concepts and methodology, despite their biological roots and motivation.

The first model studied in this thesis takes its inspiration in collaborative transport of food in the P. Longicornis ant species. We find that some key aspects of the process are well described by a graph search problem with noisy advice. The advice corresponds to characteristic short scent marks laid in front of the load in order to facilitate its navigation. In this thesis, we provide detailed analysis of the model on trees, which are relevant graph structures from a computer science standpoint. In particular our model may be viewed as a noisy extension of binary search to trees. Tight results in expectation and high probability are derived with matching upper and lower bounds. Interestingly, there is a sharp phase transition phenomenon for the expected runtime, but not when the algorithms are only required to succeed with high probability.

The second model we work with was initially designed to capture information broadcast amongst desert ants. The model uses a stochastic meeting pattern and noise in the interactions, in a way that matches experimental data. Within this theoretical model, we present in this document a strong lower bound on the number of interactions required before information can be spread reliably. Experimentally, we see that the time required for the recruitment process of even few ants increases sharply with the group size, in accordance with our result. A theoretical consequence of the lower bound is a separation between the uniform noisy PUSH and PULL models of interaction. We also study a close variant of broadcast, without noise this time but under more strict convergence requirements and show that in this case, the problem can be solved efficiently, even with very limited exchange of information on each interaction.

Soutenances de thèses
Vendredi 23 novembre 2018, 14 heures, Laboratoire MAP5, 45 rue des Saint-pères, 7eme étage, salle du conseil
Léo Planche (IRIF) Décomposition de graphes en plus courts chemins et en cycles de faible excentricité

En collaboration avec des chercheurs en biologie à Jussieu, nous étudions des graphes issus de données biologiques afin de d'en améliorer la compréhension. Ces graphes sont constitués à partir de fragments d'ADN, nommés reads. Chaque read correspond à un sommet, et deux sommets sont reliés si les deux séquences d'ADN correspondantes ont un taux de similarité suffisant. Ainsi se forme des graphes ayant une structure bien particulière que nous nommons hub-laminaire. Un graphe est dit hub-laminaire s'il peut être résumé en quelques plus courts chemins dont tous les sommets du graphe soient proche. Nous étudions en détail le cas où le graphe est composé d'un unique plus court chemin d'excentricité faible. Nous améliorons la preuve d'un algorithme d'approximation déjà existant et en proposons un nouveau, effectuant une 3-approximation en temps linéaire. De plus, nous analysons le lien avec le problème de k-laminarité défini par Michel Habib et Finn Völkel, ce dernier consistant en la recherche d'un diamètre de faible excentricité. Nous étudions ensuite le problème du cycle isométrique de plus faible excentricité. Nous montrons que ce problème est NP-complet et proposons deux algorithmes d'approximations. Nous définissons ensuite précisément la structure “hub-laminaire” et présentons un algorithme d'approximation en temps O(nm). Nous confrontons cet algorithme à des graphes générés par une procédure aléatoire et l'appliquons à nos données biologiques. Pour finir nous montrons que le calcul du cycle isométrique d'excentricité minimale permet le plongement d'un graphe dans un cercle avec une distorsion multiplicative faible. Le calcul d'une décomposition hub-laminaire permet quant à lui une représentation compacte des distances avec une distorsion additive bornée.

Soutenances de thèses
Vendredi 19 octobre 2018, 9 heures 30, Salle 580F (salle des thèses), Bâtiment Halle aux Farines
Marie Kerjean (IRIF) Reflexive spaces of smooth functions: a logical account for linear partial differential equations

Around the Curry-Howard correspondence, proof-theory has grown along two distinct fields: the theory of programming languages, for which formulas acts as data types, and the semantic study of proofs. The latter consists in giving mathematical models of proofs and programs. In particular, denotational semantics distinguishes data types which serves as input or output of programs, and allows in return for a finer understanding of proofs and programs. Linear Logic (LL) gives a logical interpretation of the basic notions of linear algebra, while Differential Linear Logic allows for a logical understanding of differentiation.

This manuscript strengthens the link between proof-theory and functional analysis, and highlights the role of linear involutive negation in DiLL. The first part of this thesis consists in an overview of prerequisites on the notions of linearity, polarisation and differentiation in proof-theory, and gives the necessary background in the theory of locally convex topological vector spaces. The second part uses two standard topologies on the dual of a topological vector space and gives two models of DiLL: the weak topology allows only for a discrete interpretation of proofs through formal power series, while the Mackey topology on the dual allows for a smooth and polarised model of DiLL. Finally, the third part interprets proofs of DiLL by distributions. We detail a polarized model of DiLL in which negatives are Fr\'echet Nuclear spaces, and proofs are distributions with compact support. We show that solving linear partial differential equations with constant coefficients can be typed by a syntax similar to the one of DiLL, which we detail.

Soutenances de thèses
Jeudi 27 septembre 2018, 15 heures 30, Salle 470E, Bâtiment Halle aux Farines
Pablo Rotondo (IRIF) Probabilistic studies in Number Theory and Word Combinatorics: instances of dynamical analysis

Dynamical Analysis incorporates tools from dynamical systems, namely the Transfer Operator, into the framework of Analytic Combinatorics, permitting the analysis of numerous algorithms and objects naturally associated with an underlying dynamical system. This dissertation presents, in the integrated framework of Dynamical Analysis, the probabilistic analysis of seemingly distinct problems in a unified way: the probabilistic study of the recurrence function of Sturmian words, and the probabilistic study of the Continued Logarithm algorithm.

Sturmian words are a fundamental family of words in Word Combinatorics. They are in a precise sense the simplest infinite words that are not eventually periodic. Sturmian words have been well studied over the years, notably by Morse and Hedlund (1940) who demonstrated that they present a notable number theoretical characterization as discrete codings of lines with irrational slope, relating them naturally to dynamical systems, in particular the Euclidean dynamical system. These words have never been studied from a probabilistic perspective. Here, we quantify the recurrence properties of a “random” Sturmian word, which are dictated by the so-called “recurrence function”; we perform a complete asymptotic probabilistic study of this function, quantifying its mean and describing its distribution under two different probabilistic models, which present different virtues: one is a naturaly choice from an algorithmic point of view (but is innovative from the point of view of dynamical analysis), while the other allows a natural quantification of the worst-case growth of the recurrence function. We discuss the relation between these two distinct models and their respective techniques, explaining also how the two seemingly different techniques employed could be linked through the use of the Mellin transform. In this dissertation we also discuss our ongoing work regarding two special families of Sturmian words: those associated with a quadratic irrational slope, and those with a rational slope (not properly Sturmian). Our work seems to show the possibility of a unified study.

The Continued Logarithm Algorithm, introduced by Gosper in Hakmem (1978) as a mutation of classical continued fractions, computes the greatest common divisor of two natural numbers by performing division-like steps involving only binary shifts and substractions. Its worst-case performance was studied recently by Shallit (2016), who showed a precise upper-bound for the number of steps and gave a family of inputs attaining this bound. In this dissertation we employ dynamical analysis to study the average running time of the algorithm, giving precise mathematical constants for the asymptotics, as well as other parameters of interest. The underlying dynamical system is akin to the Euclidean one, and was first studied by Chan (around 2005) from an ergodic, but the presence of powers of 2 in the quotients ingrains into the central parameters a dyadic flavour that cannot be grasped solely by studying this system. We thus introduce a dyadic component and deal with a two-component system. With this new mixed system at hand, we then provide a complete average-case analysis of the algorithm by Dynamical Analysis.

Soutenances de thèses
Mardi 25 septembre 2018, 14 heures, Salle 3052, Bâtiment Sophie Germain
Yann Hamdaoui (IRIF) Concurrency, References and Linear Logic

The topic of this thesis is the study of the encoding of references and concurrency in Linear Logic. Our perspective is to demonstrate the capability of Linear Logic to encode side-effects to make it a viable, formalized and well studied compilation target for functional languages in the future. The key notion we develop is that of routing areas: a family of proof nets which correspond to a fragment of differential linear logic and which implements communication primitives. We develop routing areas as a parametrizable device and study their theory. We then illustrate their expressivity by translating a concurrent λ-calculus featuring concurrency, references and replication to a fragment of differential nets. To this purpose, we introduce a language akin to Amadio’s concurrent λ-calculus, but with explicit substitutions for both variables and references. We endow this language with a type and effect system and we prove termination of well-typed terms by a mix of reducibility and a new interactive technique. This intermediate language allows us to prove a simulation and an adequacy theorem for the translation.

Soutenances de thèses
Jeudi 20 septembre 2018, 10 heures, 1828 (Olympe de Gouges)
Matthieu Boutier Routage sensible à la source

En routage next-hop, paradigme de routage utilisé dans l'Internet Global, chaque routeur choisit le next-hop de chaque paquet en fonction de son adresse destination. Le routage sensible à la source est une extension compatible du routage next-hop où le choix du next-hop dépend de l'adresse source du paquet en plus de son adresse destination. Nous montrons dans cette thèse que le routage sensible à la source est adapté au routage des réseaux multihomés avec plusieurs adresses, qu'il est possible d'étendre de manière compatible les protocoles de routage à vecteur de distance existants et que ce paradigme de routage offre avantageusement plus de flexibilité aux hôtes. Nous montrons d'abord que certains systèmes n'ordonnent pas correctement les entrées sensibles à la source dans leurs tables de routage et nous définissons un algorithme adapté aux protocoles de routage pour y remédier. Nous montrons comment étendre les protocoles à vecteur de distances au routage sensible à la source de manière compatible. Nous validons notre approche en concevant une extension d'un protocole existant (Babel), en réalisant la première implémentation complète d'un protocole sensible à la source et en utilisant ce protocole pour router un réseau multihomé. Enfin, nous montrons que le routage sensible à la source offre des possibilités de multichemin aux couches supérieures des hôtes. Nous vérifions qu'il s'intègre aux technologies existantes (MPTCP) et nous concevons des techniques d'optimisation pour les applications légères. Nous évaluons ces techniques après les avoir implémentées dans le cadre d'une application existante (mosh).

Pot en 3052 à Sophie Germain.

Soutenances de thèses
Mercredi 19 septembre 2018, 14 heures, Salle 3052, Bâtiment Sophie Germain
Laurent Feuilloley (IRIF) Certification locale en calcul distribué : sensibilité aux erreurs, uniformité, redondance et interactivité

Cette thèse porte sur la notion de certification locale, un sujet central en décision distribuée, un domaine du calcul distribué. Le mécanisme de la décision distribuée consiste, pour les nœuds d'un réseau, à décider de manière distribuée si le réseau est dans une configuration correcte ou non, selon un certain prédicat. Cette décision est dite locale, car les nœuds du réseau ne peuvent communiquer qu'avec leurs voisins. Après avoir communiqué, chaque nœud prend une décision, exprimant si le réseau est correct ou non localement, c'est-à-dire correct étant donné l'information partielle récoltée jusque-là. Le réseau est déclaré correct globalement s'il est déclaré correct localement par tous les nœuds.

Du fait de la contrainte de localité, peu de prédicats peuvent être vérifiés de cette manière. La certification locale est un moyen de contourner cette difficulté, et permet de décider tous les prédicats. C'est un mécanisme qui consiste à étiqueter les nœuds du réseau avec ce que l'on appelle des certificats, qui peuvent être vérifiés localement par un algorithme distribué. Un schéma de certification locale est correct si seuls les réseaux dans une configuration correcte peuvent être certifiés. L'idée de la certification locale est non seulement séduisante d'un point de vue théorique, comme une forme de non-déterminisme distribué, mais c'est surtout un concept très utile pour l'étude des algorithmes tolérants aux pannes, où une étape-clé consiste à vérifier l'état du réseau en se basant sur des informations stockées par les nœuds.

Cette thèse porte sur quatre aspects de la certification locale : la sensibilité aux erreurs, l'uniformité, la redondance et l'interactivité. L'étude de ces quatre sujets est motivée par une question essentielle : comment réduire les ressources nécessaires à la certification et/ou permettre une meilleure tolérance aux pannes? Pour aborder cette question, il est nécessaire de comprendre le mécanisme de certification en profondeur. Dans cette optique, dans cette thèse, nous apportons des réponses aux questions suivantes. À quel point les certificats doivent-ils être redondants, pour assurer une certification correcte? Les schémas de certification classiques sont-ils robustes à un changement de la condition de correction? Le fait d'introduire de l'interactivité dans le processus change-t-il la complexité de la certification?

Mots-clefs: Calcul distribué sur réseau, décision distribuée, certification locale, schéma d'étiquetage de preuve, tolérance aux pannes.

Soutenances de thèses
Mardi 18 septembre 2018, 14 heures, 580F (Halle aux Farines)
Guillaume Claret (IRIF) Program in Coq

In this thesis, we develop new techniques to conveniently write formally verified programs. To proceed, we study the use of Coq as a programming language in different settings. Coq being a purely functional language, we mainly focus on the representation and on the specification of impure effects, like exceptions, mutable references, inputs-outputs, and concurrency.

First, we work on two preliminary projects helping us to understand the challenges of programming in Coq. The first project, Cybele, is a Coq plugin to write efficient proofs by reflection with effects. We compile and execute the impure effects in OCaml to generate a prophecy, a kind of certificate, and then interpret the effects in Coq using the prophecy. The second project, the compiler CoqOfOCaml, imports OCaml programs with effects into Coq, using an effect inference system.

Next, we describe different generic and composable representations of impure effects in Coq. The breakable computations combine the standard exceptions and mutable references effects, with a pause mechanism to make explicit the evaluation steps in order to represent the concurrent evaluation of two terms. By implementing the Pluto web server in Coq, we realize that the most important effects to program are the asynchronous inputs-outputs. Indeed, these effects are ubiquitous and cannot be encoded in a purely functional manner. Thus, we design the asynchronous computations as a first way to represent and compile programs with events and handlers in Coq.

Then, we study techniques to prove properties about programs with effects. We start with the verification of the blog system ChickBlog written in the language of the interactive computations. This blog runs one worker with synchronous inputs-outputs per client. We verify our blog using the method of specification by use cases. We adapt this technique to type theory by expressing a use case as a well-typed co-program over the program we verify. Thanks to this formalism, we can present a use case as a symbolic test program and symbolically debug it, step by step, using the interactive proof mode of Coq. To our knowledge, this is the first such adaptation of the use case specifications in type theory. We believe that the formal specification by use cases is one of the keys to verify effectful programs, as the method of use cases proved to be convenient to express (informal) specifications in the software industry. We extend our formalism to concurrent and potentially non-terminating programs with the language of concurrent computations. Apart from the use case method, we design a model-checker to verify the deadlock freeness of concurrent computations, by compiling the parallel composition to the non-deterministic choice operator.

Soutenances de thèses
Lundi 10 septembre 2018, 14 heures, Amphi Turing, Bâtiment Sophie Germain
Luca Reggio (IRIF) Quantifiers and duality

The unifying theme of the thesis is the semantic meaning of logical quantifiers. In their basic form quantifiers allow to state the existence, or non-existence, of individuals satisfying a property. As such, they encode the richness and the complexity of predicate logic, as opposed to propositional logic.

We contribute to the semantic understanding of quantifiers, from the viewpoint of duality theory, in three different areas of mathematics and theoretical computer science. First, in formal language theory through the syntactic approach provided by logic on words. Second, in intuitionistic propositional logic and in the study of uniform interpolation. Third, in categorical topology and categorical semantics for predicate logic.

Soutenances de thèses
Jeudi 5 juillet 2018, 14 heures 30, 580F (halle aux farines)
Guillaume Lagarde (IRIF) Contributions to Arithmetic Complexity and Compression

This thesis explores two territories of computer science: complexity and compression. More precisely, in a first part, we investigate the power of non-commutative arithmetic circuits, which compute multivariate non-commutative polynomials. For that, we in- troduce various models of computation that are restricted in the way they are allowed to compute monomials. These models generalize previous ones that have been widely studied, such as algebraic branching programs. The results are of three different types. First, we give strong lower bounds on the number of arithmetic operations needed to compute some polynomials such as the determinant or the permanent. Second, we design some deterministic polynomial-time algorithm to solve the white-box polynomial identity testing problem. Third, we exhibit a link between automata theory and non-commutative arithmetic circuits that allows us to derive some old and new tight lower bounds for some classes of non-commutative circuits, using a measure based on the rank of a so-called Hankel matrix. A second part is concerned with the analysis of the data compression algorithm called Lempel-Ziv. Although this algorithm is widely used in practice, we know little about its stability. Our main result is to show that an infinite word compressible by LZ’78 can become incompressible by adding a single bit in front of it, thus closing a question proposed by Jack Lutz in the late 90s under the name “one-bit catastrophe”. We also give tight bounds on the maximal possible variation between the compression ratio of a finite word and its perturbation—when one bit is added in front of it.

Soutenances de thèses
Vendredi 27 avril 2018, 14 heures, Salle 1021, Bâtiment Sophie Germain
Alex B. Grilo (IRIF) Quantum proofs, the Local Hamiltonian problem and applications

Manuscript is available here: https://www.irif.fr/~abgrilo/thesis.pdf

Année 2017

Soutenances de thèses
Mardi 12 décembre 2017, 14 heures 30, Salle 1009, Sophie Germain
Fabian Reiter (IRIF) Distributed Automata and Logic

Developing a descriptive complexity theory for distributed computing; that was the major motivation for my PhD thesis. To clarify what this means, I will first illustrate the principle of descriptive complexity using Fagin’s theorem, and then explain how that principle can be adapted to the setting of distributed computing. After that, I will present the two main contributions of my thesis: a class of distributed automata that is equivalent to monadic second-order logic on graphs, and another class that is equivalent to a small fragment of least fixpoint logic (more specifically, to a restricted variant of the modal μ-calculus that allows least fixpoints but forbids greatest fixpoints). In both cases, the considered model of distributed computing is based on finite-state machines.

Manuscript: https://www.irif.fr/~reiterf

Soutenances de thèses
Jeudi 7 décembre 2017, 14 heures 30, Amphi 10E, Halle aux Farines
Pierre Vial (IRIF) Non-idempotent typing operators, beyond the lambda-calculus

L'objet de cette thèse est l'extension des méthodes de la théorie des types intersections non-idempotents, introduite par Gardner et de Carvalho, à des cadres dépassant le lambda-calcul stricto sensu.
  • Nous proposons d'abord une caractérisation de la normalisation de tête et de la normalisation forte du lambda-mu calcul (déduction naturelle

classique) en introduisant des types unions non-idempotents. Comme dans le cas intuitionniste, la non-idempotence nous permet d'extraire du typage des informations quantitatives ainsi que des preuves de terminaison beaucoup plus élémentaires que dans le cas idempotent. Ces résultats nous conduisent à définir une variante à petits pas du lambda-mu-calcul, dans lequel la normalisation forte est aussi caractérisée avec des méthodes quantitatives.

  • Dans un deuxième temps, nous étendons la caractérisation de la normalisation faible dans le lambda-calcul pur à un lambda-calcul infinitaire étroitement lié aux arbres de Böhm et dû à Klop et al. Ceci donne une réponse positive à une question connue comme le problème de Klop. À cette fin, il est nécessaire d'introduire conjointement un système (système S) de types infinis utilisant une intersection que nous qualifions de séquentielle, et un critère de validité servant à se débarrasser des preuves dégénérées auxquelles les grammaires coinductives de types donnent naissance. Ceci nous permet aussi de donner une solution au problème n°20 de TLCA (caractérisation par les types des permutations héréditaires). Il est à noter que ces deux problèmes n'ont pas de solution dans le cas fini (Tatsuta, 2007).
  • Enfin, nous étudions le pouvoir expressif des grammaires coinductives de types, en dehors de tout critère de validité. Nous devons encore recourir au système S et ous montrons que tout terme est typable de façon non triviale avec des types infinis et que l'on peut extraire de ces typages des informations sémantiques comme l'ordre (arité) de n'importe quel lambda-terme. Ceci nous amène à introduire une méthode permettant de typer des termes totalement non-productifs, dits termes muets, inspirée de la logique du premier ordre. Ce résultat prouve que, dans l'extension coinductive du modèle relationnel, tout terme a une interprétation non vide. En utilisant une méthode similaire, nous montrons aussi que le système S collapse surjectivement sur l'ensemble des points de ce modèle.


Soutenances de thèses
Vendredi 1 décembre 2017, 14 heures 30, Salle des Thèses, Halle aux Farines
Maxime Lucas (IRIF) Cubical categories for homotopy and rewriting

Soutenances de thèses
Vendredi 17 novembre 2017, 15 heures 15, Salle 153, Olympe de Gouges
Etienne Miquey (IRIF) Classical realizability and side-effects

Soutenances de thèses
Mardi 14 novembre 2017, 11 heures, Salle des Thèses, Halle aux Farines
Gabriel Radanne (IRIF) Tierless Web programming in ML

Eliom est un dialecte d’OCaml pour la programmation Web qui permet, à l’aide d’annotations syntaxiques, de déclarer code client et code serveur dans un même fichier. Ceci permet de construire une application complète comme un unique programme distribué dans lequel il est possible de définir des widgets aisément composables avec des comportements à la fois client et serveur. Eliom assure un bon comportement des communications grâce à un système de type et de nouvelles constructions adaptés à la programmation Web. De plus, Eliom est efficace : un découpage statique sépare les parties client et serveur durant la compilation et évite de trop nombreuses communications entre le client et le serveur. Enfin, Eliom supporte la modularité et l’encapsulation grâce à une extension du système de module d’OCaml permettant l’ajout d’annotations indiquant si une définition est présente sur le serveur, le client, ou les deux. Cette thèse présente la conception, la formalisation et l’implémention du langage Eliom.


Soutenances de thèses
Mardi 27 juin 2017, 10 heures, Salle 255, Olympe de Gouges
Amina Doumane (IRIF) On the infinitary proof theory of logics with fixed points

Année 2016

Soutenances de thèses
Vendredi 9 décembre 2016, 14 heures, Salle des Thèses, Halle aux Farines
Cyrille Chenavier (IRIF) Le treillis des opérateurs de réduction : applications aux bases de Gröbner non commutatives et en algèbre homologique

Soutenances de thèses
Mardi 11 octobre 2016, 14 heures, Salle 1006, Sophie Germain
Wenjie Fang (IRIF) Aspects énumératifs et bijectifs des cartes combinatoires : généralisation, unification et application

Le sujet de cette thèse est l'étude énumérative des cartes combinatoires et ses applications à l'énumération d’autres objets combinatoires.

Les cartes combinatoires sont un modèle combinatoire riche. Elles sont définies d’une manière intuitive et géométrique, mais elles sont aussi liées à des structures algébriques plus complexes. À la rencontre de différents domaines, les cartes peuvent être analysées par une grande variété de méthodes, et leur énumération peut aussi nous aider à compter d’autres objets combinatoires. Cette thèse présente un ensemble de résultats et de connexions très riches dans le domaine de l’énumération des cartes. Les résultats dans cette thèse se divise en deux grandes parties. La première partie contient mes travaux sur l'énumération des constellations, en utilisant les caractères du groupe symétrique ou bien en résolvant des équations fonctionnelles sur leur séries génératrices. La deuxième partie est sur le lien énumératif entre les cartes et d’autres objets combinatoires, par exemple les généralisations du treillis de Tamari et les graphes aléatoires qui peuvent être plongés dans une surface donnée.


Soutenances de thèses
Vendredi 8 avril 2016, 10 heures, Salle 2011, Sophie Germain
Charles Grellois (IRIF) Sémantique de la logique linéaire et model-checking d'ordre supérieur