Institut de Recherche en Informatique Fondamentale (IRIF)

CNRS

Université Paris Cité

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.

Suivez nous sur Mastodon, Twitter/X et LinkedIn :

LinkedIn Twitter/X Mastodon

22.1.2025
Le troisième Paris ACTS, aura lieu à l'IRIF, le mercredi 29 janvier. P-ACTS est une série de séminaires centrés sur les connexions entre la théorie des automates et la théorie de la concurence, partagés entre l'EPITA, l'IRIF et le LIX. Les deux intervenants seront Laetitia Laversa et Glynn Winskel. Les conférences seront également diffusées sur Zoom. Pour les résumés et plus d'informations sur le séminaire, voir cette page:

7.1.2025
Nous sommes heureux d'accueillir notre nouvelle responsable financière et comptable, Chafia Dordoigne. Vous pouvez la rencontrer dans le bureau 4002.

6.1.2025
L'IRIF vous souhaite une excellente année, riche en découvertes scientifiques, en succès académiques et en épanouissement personnel !

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 :

csl2024.jpg

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.

popl_2025.jpg

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.


(Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.)

Preuves, programmes et systèmes
Jeudi 23 janvier 2025, 10 heures, Amphithéâtre Alan Turing du bâtiment Sophie Germain
Nathanaëlle Courant (INRIA Paris and OCamlPro) An efficient and verified convertibility check in dependent type theory

The convertibility test, which checks if two λ-terms are equal up to β-reduction, is an essential part of typechecking and proof verification in proofs assistants based on type theory, such as Coq, Agda and Lean. Naturally, the correctness of such a test is necessary to ensure the proofs thus verified are valid; but having an efficient test is also required both for real-time interaction with the user, and for proof search.

In this presentation, we start with an efficient, strong call-by-need, big-step semantics for the λ-calculus, which is the critical building block to implement a convertibility test in a classical manner. We then show how we can improve upon this by considering the convertibility problem in its entirety, viewing it as proof search. To this end, we study what can be considered a (non-)convertibility proof, drawing upon existing work.

This gives rise to a new parallel, heuristic-less algorithm for this test, which does not duplicate computations, and comes with worst-case complexity guarantees. We derived a virtual machine from this algorithm, and made it more efficient by following Grégoire and Leroy, showing that our algorithm is suited to compilation of the input λ-terms for additional efficiency. Both this semantics and this efficient parallel convertibility test have been implemented in OCaml and experimentally validated, significantly outperforming Coq in some cases. They are also both formalised and verified using Coq, building confidence in our work.

Séminaire des membres non-permanents
Jeudi 23 janvier 2025, 16 heures, Salle 3052
Miriam Marzaioli CANCELED. A Crèche Introduction to Cohen's Forcing

This talk has been canceled due to an unexpected issue of the speaker. We apologize.

In 1963, Paul Cohen discovered the forcing method and definitively answered the first of Hilbert's 23 problems by using this technique to prove the independence of the Continuum Hypothesis from the ZFC axioms. Since then, forcing has become the primary tool in set theory for establishing independence and consistency results. In this talk, we will present the key ingredients and ideas necessary to understand Cohen's model of ZFC + ¬CH. In particular, we will explore Cohen's forcing via the boolean-valued models approach.

La syntaxe rencontre la sémantique
Jeudi 23 janvier 2025, 13 heures 30, Salle 3052
Gabriele Tedeschi (Univ. Pisa) Modelling Quantum Protocols: a Novel Semantics with Quantum Probabilities

Quantum protocols involve a number of features like concurrent execution, quantum primitives, message communication and non-determinism. The well-studied calculi and models for probabilistic concurrent systems seem inadequate in the quantum setting, as they do not comply with the observational limitations of quantum theory. We will explore a new semantic model made of “Quantum Distributions” and “Quantum Transition Systems”, instead of probability distributions and probabilistic LTSs. We provide a symbolic, quantum semantics for a minimal quantum process calculus, which we prove sound and complete with respect to the known ground, probabilistic behaviour of quantum processes.

Automates
Vendredi 24 janvier 2025, 14 heures, Salle 3052
Olivier Carton (IRIF) Rauzy dimension and finite state dimension

In a paper of 1976, Rauzy studied two complexity notions, $\underline{β}$ and $\overline{β}$, for infinite sequences over a finite alphabet. The function $\underline{β}$ is maximum exactly in the Borel normal sequences and $\overline{β}$ is minimum exactly in the sequences that, when added to any Borel normal sequence, the result is also Borel normal. Although the definition of $\underline{β}$ and $\overline{β}$ do not involve finite-state automata, we establish some connections between them and the lower $\underline{\dim}$ and upper $\overline{\dim}$ finite-state dimension (or other equivalent notions like finite-state compression ratio, entropy or cumulative log-loss of finite-state predictors). We show tight lower and upper bounds on $\underline{\dim}$ and $\overline{\dim}$ as functions of $\underline{β}$ and $\overline{β}$, respectively. In particular this implies that sequences with $\overline{\dim}$ zero are exactly the ones that that, when added to any Borel normal sequence, the result is also Borel normal. We also show that the finite-state dimensions $\underline{\dim}$ and~$\overline{\dim}$ are essentially subadditive.

Vérification
Lundi 27 janvier 2025, 11 heures, 3052 and Zoom link
Enrico Bini (University of Turin) Cutting the Unnecessary Deadlines in EDF

Together with Fixed Priority Scheduling, Earliest Deadline First (EDF) is the second leg on top of which a large portion of the research on real-time systems stands. At the heart of the EDF exact schedulability test, a pivotal role is played by the demand bound function test, which requires to evaluate whether the amount of work required to complete a set of jobs is less than or equal to the amount of time available. Such a test is checked over a set of time instants.

In this work, it is proposed a method that cuts drastically the set of constraints to be checked. Such a method is applicable also to tasks with release offset. Notably, it is proved that such a reduced set of constraints is minimal: it is not possible to reduce the set any further without losing the sufficiency of the test. The code to make this reduction is publicly available on GitHub.

Programmation
Lundi 27 janvier 2025, 10 heures, 3071
Jules Viennot (IRIF) Implementation of purely functional catenable double-ended queue

Twenty-five years ago, Kaplan and Tarjan established a striking result: there exist “purely functional, real-time deques with catenation”. In other words, there exists a data structure that supports the following operations: “push” and “pop” which insert and extract one element at the front end, “inject” and “eject” which insert and extract one element at the rear end and “concat”, the concatenation operation. Moreover, the data structure is persistent: none of the five operations modifies or destroys its argument. Finally, each operation has worst-case time complexity O(1). This presentation will provide an overview of the first ever implementation of the data structure, done in OCaml, and its verification in Rocq.

Algorithmique distribuée et graphes
Mardi 28 janvier 2025, 15 heures, 3052
Gil Puig I Surroca (Université Paris Dauphine) Endomorphism monoids of regular graphs

Back in 1939, Frucht proved that every finite group is isomorphic to the automorphism group of a finite graph. This incited an examination of the influence that standard graph theoretical concepts can have on automorphism groups. Eventually, the framework was enlarged by extending the analyses to endomorphism monoids. This has ultimately established a particular connection between semigroup classes and graph classes, notably in terms of sparsity and combinatorial regularity. The goal of the presentation is to contextualize a new result on endomorphism monoids of regular graphs that adds some detail to the picture. This is joint work with Kolja Knauer.

Sémantique
Mardi 28 janvier 2025, 15 heures, Salle 3071
Rémi Di Guardia A simple proof of sequentialization for proof-nets, and links with graph theory

Proof-nets are a major contribution from linear logic. Contrary to the usual representation of proofs as derivation trees in sequent calculus, proof-nets represent proofs as general graphs respecting some correctness criterion. A standard result is that these two syntaxes correspond to each other, which is called sequentialization. Despite being a well-known theorem, its proofs in the literature are generally complex. I will present a new simple proof for proof-nets of multiplicative linear logic, modular enough to still apply in the presence of the mix-rule. Then, I will develop links between sequentialization and more general graph theory, following on works from Rétoré and Nguyễn but focusing on edge-colored graphs instead of perfect matchings.

[Joint work with Olivier Laurent, Lorenzo Tortora de Falco and Lionel Vaux Auclair]

Séminaire des membres non-permanents
Jeudi 30 janvier 2025, 16 heures, Salle 3052
Manu Catz Number Systems and Oriented Shapes

Decimal writing is just one way of notating the natural numbers, but we can as well consider the “first” ways of doing so: unary writing (the tally system), binary writing (the language of classical computers) or even ternary writing (examples welcomed!). Unary gives a natural labelling on the family of simplices (the family to which belongs the triangle, the tetrahedron,…) and furthermore a way of orienting any dimensional face of such shapes. Likewise, binary is the natural choice to label and orient the family of cubes (the square, the cube,…). In this talk I will show these constructions, as well as how this particular labelling allows us to easily construct simplices from cubes and cubes from simplices. Lastly, I will address the elephant in the room: what gets labelled and oriented by ternary ?!

There are no prerequisites for the content of this talk more than a basic understanding of binary, however these ideas come from higher category theory and type theory, in particular work by Street and Aitchison on the oriented simplices and cubes respectively, as well as work by Ara, Lafont and Métayer to better uncover these constructions, and the notion of parametricity as presented by Herbelin and Ramachandra.

Automates
Vendredi 31 janvier 2025, 14 heures, Salle 3052
Christian Choffrut Message complexity of multiautomata systems

The model, due to Jurdzinski in his PhD thesis 1999 under the direction of Kutylovski, is a finite collection of one-way or two-way deterministic automata working synchronously on the same input and dispatching messages when reaching certain so-called broadcasting states. The input is accepted if a predetermined automaton reaches a final state when it arrives at the right end of the input. The message complexity of the system is the function f(n) which, to every integer, assigns the minimum number of messages required in a run over inputs of length n.

Jurdzinski and Kutylovski, 2002, proved in the one-way case that if the system requires a nonconstant number of messages then it requires at least log(n) messages and claimed a result of the same kind for two-way systems.

I show that when the input is unary, i.e., over an alphabet with a unique letter, the language accepted is rational (or equivalently ultimately periodic) if and only if the number of messages is finite.