Bienvenue L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris Cité, et héberge une équipe-projet Inria. Les recherches menées à l'IRIF reposent sur l’étude et la compréhension des fondements de toute l’informatique, afin d’apporter des solutions innovantes aux défis actuels et futurs des sciences numériques. L'IRIF regroupe près de deux cents personnes. Sept de ses membres ont été lauréats de l'European Research Council (ERC), trois sont membres de l'Institut Universitaire de France (IUF), deux sont membres de l'Academia Europæa, et un est membre de l'Académie des sciences. Notion du jour Réseaux Sociaux Suivez nous sur Mastodon, Twitter/X et LinkedIn : Actualités 11.12.2024 Le lundi 16 décembre 2024, SOC² organise une journée dédiée aux modèles de calcul basés sur les flots de données pour célébrer l'anniversaire du célèbre article de Gilles Kahn sur les KPN, intitulé « The semantics of a simple language for parallel programming », publié en 1974. L'objectif est d'explorer les divers domaines de recherche introduits par cet article. La journée débutera par une présentation de l'article original. Le programme ainsi que le lien d'inscription (gratuit) sont disponibles ici : 26.11.2024 Félicitations aux membres de l'IRIF suivants dont les articles ont été acceptés pour la conférence POPL 2025 : Rida Ait El Manssour, Guillaume Baudart, Adrienne Lancelot, Giulio Manzonetto, Gabriel Scherer et Mahsa Shirmohammadi. 28.11.2024 Le prix Ackermann récompense des thèses exceptionnelles en logique informatique lors de la conférence ACSL. Cette année, le prix a été attribué à deux thèses encadrées à l'IRIF : les lauréats sont Gaëtan Douéneau-Tabot, encadré par Olivier Carton et Emmanuel Filiot à l'Université Paris-Cité (France), et Aliaume Lopez, encadré par Jean Goubault-Larrecq et Sylvain Schmitz à l'ENS Paris-Saclay et à l'Université Paris-Cité (France), respectivement. Ils recevront leur prix à CSL 2025, à Amsterdam, qui aura lieu du 10 au 14 février 2025. 31.10.2024 L’IRIF est ravi d’accueillir Dexter Kozen de l’Université Cornell en tant qu'intervenant de nos Distinguished Talks. La conférence aura lieu le 3 décembre 2024 à partir de 11h. Plus de détails à venir ! 12.11.2024 La journée du Groupe de Travail LVP (Langages et à la Vérification de Programme) du GdR GPL du CNRS se déroulera le jeudi 14 novembre 2024 à l'IRIF, de 9h à 17h40. Emilio Jesús Gallego Aria, chercheur Inria à l'IRIF, Université de Paris donnera d'ailleurs un exposé sur : “Flèche: Incremental Validation for Hybrid Formal Documents”. Cet évènement est gratuit mais l'inscription est obligatoire. 5.11.2024 Cette année, trois chercheurs de l'IRIF font partie de deux projets ayant été retenus pour une bourse Synergie 2025 du Conseil Européen de la Recherche (ERC). Toutes nos félicitations à Valérie Berthé, Hugo Herbelin et Paul-André Melliès ! Nous leur souhaitons d'obtenir des résultats concluants. 18.10.2024 Nous souhaitons la bienvenue à Mélissa Goddé, nouvelle gestionnaire, qui vient renforcer l'équipe administrative. 24.10.2024 L'informatique a-t-elle un avenir ? Telle est la question qui sera débattue lors de la troisième conférence “On éteint, on réfléchit, on discute”, organisée à l'Université Paris Cité par François Laroussinie. José Halloy (LIED) et Anne-Laure Ligozat (LISN) sont les conférenciers invités. Elle se tiendra le mardi 10 décembre 2024, de 16h15 à 18h30. Cet événement est gratuit. edit toutes les anciennes actualités (Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.) Agenda Automates Vendredi 13 décembre 2024, 14 heures, Salle 3052 Vincent Michielini (University of Warsaw) Complexity of query entailment for description logic with transitive roles In description logic, the query entailment problem asks the following question: given an ABox A (i.e. basic finite structure, to be completed), an ontology T (or a TBox, a finite set of constrains), and a request q (= a conjunctive query, = a subgraph), does any structure satisfying the ABox and the ontology necessarily also satisfy the request? In ALC, the basic description logic (which is nothing more than modal logic in disguise), this problem is well understood, as it is known to be ExpTime-complete in combined complexity, and coNP-complete in data complexity (i.e. with TBox and query fixed) [Lutz '08]. However, the exact complexity for S, the extension of ALC where some roles (= binary relations) are specified to be transitive, was not known yet. The status being that the problem is coNExpTime-hard [Eiter et al. '09] and in 2ExpTime [Calvanese et al. '98]. An article of 2010 tried to close the gap in a special case, but sadly contains a technical mistake, which could not be repaired so far [personal communication]. In this seminar, we propose an alternative solution to the problem, that even works in the most general case: we prove that if the entailment does not hold, then there exists a counter-model admitting a representation of exponential size (although being most possibly infinite). Hence, we conclude that the query entailment for S is indeed coNExpTime-complete. The construction of such a counter-model elegantly implies a variant of automata over infinite trees. Soutenances de thèses Lundi 16 décembre 2024, 10 heures, Salle 3052 Avinandan Das (IRIF, CNRS, Universite Paris Cite) Computation with Partial Information : An Algorithmic Investigation of Graph Problems in Distributed Computing and Streaming This thesis discusses the paradigm of computation with partial information, which is necessitated by the infeasibility of processing massive datasets in their entirety. Traditional algorithms, which require full access to input data, become impractical for large-scale problems due to time and space constraints. Several models of computation that allow for partial or incomplete data access, such as property testing, data stream models, distributed computing, and massively parallel computing, have been proposed in the literature. This thesis deals with two models, the distributed LOCAL model and the data stream model in this paradigm. In the LOCAL model, we extend existing frameworks for the well-studied problem of $(\Delta+1)$-proper coloring to a more generalized $k$-partial $(k+1)$-coloring problem, providing novel algorithms and complexity results. Given a $n$-node graph $G=(V,E)$, a $k$-partial $c$-coloring asks for a coloring of the vertices with colors in $\{1,\dots,c\}$, such that every vertex $v\in V$ has at least $\min\{k,\deg(v)\}$ neighbors with a color different from its own color. We extend the rounding based algorithm of Ghaffari and Kuhn (2020), to give a $O(\log n\cdot \log^3k)$ round algorithm and a $O(\log n\cdot \log^2k)$ round algorithm for $k$-partial list coloring and $k$-partial $(k+1)$-coloring respectively. In the data stream model, we introduce the {\em certification} of solutions to computing problems when access to the input is restricted. This topic has received a lot of attention in the distributed computing setting, and we introduce it here in the context of \emph{streaming} algorithms, where the input is too large to be stored in memory. Given a property $P$, a \emph{streaming certification scheme} for $P$ is a \emph{prover-verifier} pair where the prover is a computationally unlimited but non-trustable oracle, and the verifier is a streaming algorithm. For any input, the prover provides the verifier with a \emph{certificate}. The verifier then receives its input as a stream in an adversarial order and must check whether the certificate is indeed a \emph{proof} that the input satisfies $P$. The main complexity measure for a streaming certification scheme is its \emph{space complexity}, defined as the sum of the size of the certificate provided by the oracle, and of the memory space required by the verifier. We give streaming certification schemes for several graph properties, including maximum matching, diameter, degeneracy, and coloring, with space complexity matching the requirement of \emph{semi-streaming}, i.e., with space complexity $O(n\, \mbox{polylog}\, n)$ for $n$-node graphs. For each of these properties, we provide upper and lower bounds on the space complexity of the corresponding certification schemes, many being tight up to logarithmic multiplicative factors. We also show that some graph properties are hard for streaming certification, in the sense that they cannot be certified in semi-streaming, as they require $\Omega(n^2)$-bit certificates. The results presented in this thesis contribute to the growing body of work on algorithms for large datasets, particularly in the contexts of graph theory and distributed systems, and open new avenues for future research in computation with partial information. Formath Lundi 16 décembre 2024, 14 heures, 3052 et en visio Meven Lennon-Bertrand (Cambridge) MetaCoq tutorial Coq is a programming language: have you ever dreamed of using it to program itself? Even better, to certify said programs? MetaCoq does just that (and much more). Let's have a tour together! If you want to play around live, I recommend installing the coq-metacoq-template opam package beforehand, and to check that you can step through this file: https://github.com/MetaCoq/tutorials/blob/main/popl24/exercises/MetaCoqPrelude.v Algorithmes et complexité Mardi 17 décembre 2024, 11 heures, Salle 3052 Team Event AlgoComp lightning talks ⚡️ Soutenances de thèses Mardi 17 décembre 2024, 14 heures, Salle 3052, Bâtiment Sophie Germain Maël Luce Distributed Randomized and Quantum Algorithms for Cycle Detection in Networks Distributed computing encompasses all models where a set of computing entities have to collectively solve a problem while each detaining private inputs. This field of theoretical computer science then underlies many real situations: multi-core processors, servers and clouds, the internet, swarms of robots, cars or other intelligent objects, and any network in which entities have some kind of independence. This thesis is dedicated to studying the impact of limited bandwidth on the ability to solve “local problems” in distributed networks. More precisely, in a graph-network where the amount of information exchanged between two neighbors is limited over time, how long does it take to detect a cycle ? First we study a state of the art algorithm for the detection of small even cycles and show that this technique becomes unefficient for bigger lengths of cycles. For any even length of cycle bigger than 10, there exists a family of graphs of growing size in which this technique cannot detect a cycle in a reasonable time. Then, we exhibit a new algorithm that matches and extends the complexity of the previously mentioned one to all even lengths of cycles. To prove its correctness, we establish a general graph combinatorics result. It can be seen as a lower bound of the “local density” in a graph without a 2k-cycle. Finally, we develop a new framework for quantum distributed computing: the distributed quantum Monte-Carlo amplification. It helps us quantumly speed up our even-length cycle detection algorithm. This same technique can also be applied to speed up other cycle detection problems in the litterature. Soutenances de thèses Mardi 17 décembre 2024, 17 heures, Salle 3052, Bâtiment Sophie Germain & Zoom Félix Castro The ramified analytic hierarchy in second-order logic In its first part, this thesis focuses on the study of the ramified analytic hierarchy (RAH) in second-order arithmetic (PA2). The ramified analytic hierarchy was defined by Kleene in 1960. It is an adaptation of the notion of constructibility (introduced by G¨odel for set theory) to the framework of second-order arithmetic. The properties of this hierarchy, in relation to computability and to the study of set-theoretic models of PA2, have been studied in depth. It seems natural to formalize RAH in PA2 in an attempt to demonstrate that adding the axiom of choice or (a variant of) the axiom of constructibility to second-order arithmetic does not bring contradiction. However, the only written trace of such a formalization seems to be incorrect. In this thesis, we want to work on this formalization. To do this, we will work in a version of arithmetic obtained by removing the axiom of induction from the axioms of PA2. In this system, a new variant of the axiom of choice appears: we call it the axiom of collection, in reference to the homonymous axiom of set theory. It seems that this axiom has never been considered in the context of second-order logic. We show that it has good computational properties: its contrapositive is realized by the identity in classical realizability, while it is itself realized by the identity in intuitionistic realizability. In addition, we show that it is equivalent to an axiom which is well-behaved with respect to a negative translation from classical logic into intuitionistic logic. Finally, we show that this variant of the axiom of collection is weaker than a variant of the axiom of choice in intuitionistic logic. We therefore work in a theory without induction but containing the axiom of collection. We aim at studying the ramified analytic hierarchy. We show that it is a model of PA2 satisfying a strong version of the axiom of choice: the principle of the well-ordered universe. It seems that the axiom of collection is necessary to prove this result and we will thoroughly explain this intuition. In the second part of the thesis, shorter than the first, we study extensional equality in finite type arithmetic. Higher Type Arithmetic (HAω) is a first-order many-sorted theory. It is a conservative extension of Heyting Arithmetic obtained by extending the syntax of terms to all of System T: the objects of interest here are the functionals of higher types. While equality between natural numbers is specified by the axioms of Peano, how can equality between functionals be defined? From this question, different versions of HAω arise, such as an extensional version (E-HAω) and an intentional version (I-HAω). In this work, we will see how the study of partial equivalence relations leads us to design a translation by parametricity from E-HAω to HAω. Preuves, programmes et systèmes Jeudi 19 décembre 2024, 10 heures 30, Salle 3052 & online (Zoom link) Dominik Kirst (IRIF) Applied Synthetic Computability Theory: Gödel’s Incompleteness Theorem and Post’s Problem Traditionally, computability theory is based on a notion of computable functions induced by concrete models like Turing machines, lambda calculus, or general recursion. While these models are well-studied, they only provide a somewhat secondary explanation of computability, at times obscuring the simple computational essence of abstract constructions and constituting a notorious burden for mechanisation in a proof assistant. In this talk, I will give an overview of synthetic computability theory as introduced by Richman and Bauer, offering an elegant alternative: at the price of giving up on some principles of classical reasoning, computability becomes a primitive notion, even internalisable by the axiom that every function is computable. After discussing this general framework in the context of constructive mathematics, I will describe some recent work on Gödel’s incompleteness theorem and Post’s problem both developed synthetically in constructive type theory and mechanized in the Coq proof assistant. Soutenances de thèses Jeudi 19 décembre 2024, 14 heures, Amphithéâtre Turing, Bâtiment Sophie Germain Srinidhi Nagendra Automated testing of distributed protocol implementations The growth of modern internet is enabled by large-scale, highly available, and resilient distributed systems. These systems allow data to be replicated globally while ensuring availability under failures. To ensure reliability and availability in the presence of failures, the systems rely on intricate distributed protocols. Yet in practice, bugs in the implementations of these distributed protocols have been the source of many downtimes in popular distributed databases. Ensuring the correctness of the implementations remains a significant challenge due to the large state space. Over the years, many techniques have been developed to ensure the correctness of the implementations ranging from systematic model checking to pure random exploration. However, a developer testing the implementation with current techniques has no control over the exploration. In effect, the techniques are agnostic to the developer's knowledge of the implementation. Furthermore, very few approaches utilize the formal models of the protocols when testing the implementations. Efforts put into modeling and verifying the correctness of the model are not leveraged to ensure the correctness of the implementation. To address these drawbacks, in this thesis, we propose 3 new approaches to test distributed protocol implementations - Netrix, WaypointRL, and ModelFuzz. The first two techniques - Netrix and WaypointRL are biased exploration approaches that accept developer input. Netrix is a novel unit testing algorithm that allows developers to bias the exploration of an existing testing algorithm. A developer writes low-level filters in a domain-specific language to fix specific events in an execution that are enforced by Netrix. WaypointRL improves on Netrix to accept high-level state predicates as waypoints and uses reinforcement learning to satisfy the predicates. WaypointRL is effective in biasing the exploration while requiring less effort from the developer. Using popular distributed protocol implementations, we show that additional developer input leads to effective biased exploration and improved bug-finding capabilities. The third technique - ModelFuzz - is a new fuzzing algorithm that bridges the gap between the model and the implementation of the protocol. We use model states as coverage to guide input generation that are then executed on the implementation. We show with three industrial benchmarks that existing coverage notions are insufficient for testing distributed systems and that using TLA+ model coverage to test implementations leads to discovering new bugs. Sémantique Mardi 7 janvier 2025, 15 heures, Salle 3071 Thomas Ehrhard Upper approximating probabilities of convergence of PCF programs, using extensional probabilistic coherence spaces Probabilistic coherence spaces (PCSs) provide an adequate, and actually fully abstract, denotational model of probabilistic PCF (an idealised Turing complete functional language extended with probabilistic choice). Given a closed probabilistic PCF term M of type bool for instance, PCSs provide therefore a way to approximate from below the probability p that M reduces, eg, to true. I will show how, extending PCSs with an “extensional structure”, it is also possible to approximate this probability p from above. These extensional PCSs form a model of LL, and are a probabilistic analog of Berry's bidomains. I will explain how this approximation mechanism can be straightforwardly implemented using a Krivine Machine which computes finite approximants of a powerseries associated with M by the extensional PCS semantics. If time permits, there will be a demo. Catégories supérieures, polygraphes et homotopie Vendredi 10 janvier 2025, 14 heures, Salle 1013 Léo Hubert Correspondances de Dold-Kan homotopiques