Institut de Recherche en Informatique Fondamentale (IRIF)

CNRS

Université Paris Cité

IRIF is a research laboratory of CNRS and Université Paris Cité, also hosting one Inria project-team.

The research conducted at IRIF is based on the study and understanding of the foundations of all computer science, in order to provide innovative solutions to the current and future challenges of digital sciences.

IRIF hosts about 200 people. Seven of its members have been distinguished by the European Research Council (ERC), six are members of the Institut Universitaire de France IUF), two are members of the Academia Europæa, and one is member of Académie des sciences.

Follow us on Twitter/X, LinkedIn and Mastodon for our latest news:

LinkedIn Twitter/X Mastodon

11.12.2024
Monday, 16 December 2024, SOC² is organizing a day dedicated to dataflow models of computation to celebrate the anniversary of the famous paper of Gilles Kahn on KPN, entitled « The semantics of a simple language for parallel programming » was published in 1974. The goal is to travel through the various research fields that has been opened by this paper. The original paper will be presented to start the day. The program and the registration link (free of charge) is here:

csl2024.jpg

28.11.2024
The Ackermann Award recognizes outstanding dissertations for Logic in Computer Science at ACSL conference. This year, the prize has been awarded to two thesis supervised at IRIF: the laureates are Gaëtan Douéneau-Tabot supervised by Olivier Carton and Emmanuel Filiot at Université Paris-Cité (France) and Aliaume Lopez supervised by Jean Goubault-Larrecq and Sylvain Schmitz at ENS Paris-Saclay and Université Paris-Cité (France), respectively. They will receive their prize to CSL 2025, in Amsterdam, which will take place from 10 to 14 February 2025.

popl_2025.jpg

26.11.2024
Congratulations to our following members whose papers have been accepted for the 2025 POPL conference : Rida Ait El Manssour, Guillaume Baudart, Adrienne Lancelot, Giulio Manzonetto, Gabriel Scherer and Mahsa Shirmohammadi

12.11.2024
The LVP (Languages and Program Verification) working group of the GPL GdR of the CNRS will be holding its one-day conference on Thursday 14 November 2024 at IRIF, from 9am to 5.40pm. Emilio Jesús Gallego Aria, Inria researcher at IRIF, University of Paris, will be giving a talk on : ‘Flèche: Incremental Validation for Hybrid Formal Documents’. This event is free but registration is required.

5.11.2024
This year, three IRIF researchers are part of two projects that have won a 2025 Synergy Grant from the European Research Council (ERC). Many congratulations to Valérie Berthé, Hugo Herbelin and Paul-André Melliès ! IRIF wishes them successful results.

24.10.2024
Does Computer Science Have a Future? That is the question to be debated during the third conference, “We Turn Off, We Reflect, We Discuss,” organized at Université Paris Cité by François Laroussinie. José Halloy (LIED) and Anne-Laure Ligozat (LISN) are the invited speakers. It will take place on December 10, 2024, from 4:15 PM to 6:30 PM. This event is free of charge.

perso-sergio-rajsbaum.jpg

24.10.2024
The Innovation Prize has been awarded to Sergio Rajsbaum, associate member of IRIF, in recognition of his significant contribution to Distributed Computing. The prize will be presented to him at the SIROCCO'25 conference in Delphi, Greece.

pp_melissa_godde.jpg

18.10.2024
We welcome Mélissa Goddé, the new administrative assistant, who has joined the administrative team.

(These news are displayed using a randomized-priority ranking.)

Automata
Friday December 13, 2024, 2PM, 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.

PhD defences
Monday December 16, 2024, 10AM, 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
Monday December 16, 2024, 2PM, 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

Algorithms and complexity
Tuesday December 17, 2024, 11AM, Salle 3052
Team Event AlgoComp lightning talks ⚡️

PhD defences
Tuesday December 17, 2024, 2PM, 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.

PhD defences
Tuesday December 17, 2024, 5PM, 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ω.

Proofs, programs and systems
Thursday December 19, 2024, 10:30AM, 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.

PhD defences
Thursday December 19, 2024, 2PM, 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.

Semantics
Tuesday January 7, 2025, 3PM, 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.

Higher categories, polygraphs and homotopy
Friday January 10, 2025, 2PM, Salle 1013
Léo Hubert Correspondances de Dold-Kan homotopiques