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é, qui 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. Six de ses membres ont été lauréats de l'European Research Council (ERC), six 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.

École de Printemps d’Informatique Théorique 2023

24.3.2023
The 50th edition of EPIT (École de Printemps d’Informatique Théorique) will have as theme The Kaleidoscope of Complexity Theory and will take place on June 12-16, 2023 at the Vieille Perrotine CAES/CNRS holiday center on the Oléron Island, in France.

Interview PhD thesis Farzad Jafarrahmani

6.3.2023
Farzad Jafarrahmani, former PhD student at IRIF explains his thesis Fixpoints of Types in Linear Logic from a Curry-Howard-Lambek Perspective in this written interview.

Appel à manifestation d'intérêt 2023 - Médiation scientifique

7.3.2023
Pour la troisième année consécutive, la Faculté des Sciences d’Université Paris Cité lance un appel à manifestation d’intérêt pour accompagner et soutenir ses membres dans leurs initiatives ayant vocation à rendre accessible un sujet de recherche scientifique à un public non spécialiste. Date limite 20 mars 2023 minuit.

Journées Nationales du GDR IM 2023

10.3.2023
Les prochaines Journées Nationales du GDR IM (JNIM 2023) auront lieu à l'Université Paris Cité du 4 avril au 7 avril et sont organisées par l'IRIF. Programme et inscription ici.

JACM Articles from 2022

7.3.2023
The paper “Decentralized Asynchronous Crash-resilient Runtime Verification” authored by Borzoo Bonakdarpour (MSU), Pierre Fraigniaud (IRIF), Sergio Rajsbaum (UNAM), David Rosenblueth (UNAM), and Corentin Travers (LIS) has been selected in the “sample of [eight] exciting [..] articles on a diverse range of topics that were published in 2022” in the Journal of the ACM (JACM).

Conférence vidéo “Manuel de Cryptanalyse à l’usage de la NSA”

6.3.2023
“Manuel de Cryptanalyse à l’usage de la NSA” est une conférence ludique, présentée par Sylvain Perifel – Maître de conférences (Université Paris Cité/IRIF) à l’occasion de l’édition 2022 de la Fête de la Science. Elle retrace et met en pratique les différentes avancées historiques de cette science, du code de César à RSA en passant par les substitutions mono-alphabétiques et par le chiffre de Vigenère.

Shared engineer position in formal methods

27.2.2023
Shared engineer position in formal methods, between IRIF, LIPN and LMF. Deadline to apply: 17/03/2023.


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

Algorithmique distribuée et graphes
Mercredi 29 mars 2023, 14 heures, 3052
Valentin Bartier (LIRIS) Independent set reconfiguration in sparse graphs

The problem of reconfiguring independent sets belongs to the broader field of combinatorial reconfiguration problems. It can be formulated as follows: given a collection of tokens placed on the vertices of an independent set of a graph, is it possible to move one by one these tokens to another target independent set, such that two tokens are never neighbors throughout the transformation? After a general introduction to combinatorial reconfiguration and the independent set reconfiguration problem, we will focus on the “Token Sliding” variant. In this variant, one step of the transformation consists in moving a token from a vertex to a neighboring vertex. We will focus on the parameterized complexity of this problem in sparse classes of graphs and on the new tools we have recently designed for the development of FPT algorithms.

Analyse et conception de systèmes
Mercredi 29 mars 2023, 14 heures, Salle 1007
François Pottier (Inria) Sémantiques monadiques et sémantiques à pas amples

Dans cet exposé très informel à propos d'un travail en cours, je souhaiterais discuter de différents styles pour définir (en Coq) la sémantique d'un langage de programmation. Une de mes motivations est d'obtenir une sémantique au moins partiellement exécutable dans Coq et d'en tirer un mécanisme d'exécution symbolique qui pourrait être exploité dans un système de vérification de programmes.

Au cours de l'exposé, je présenterai deux styles de sémantique (pour un langage sans effets de bord, hormis divergence et plantage), et au-dessus de chacun d'eux, je construirai une logique de Hoare. Le premier style, “monadique jusqu'au bout”, reproduit des idées que l'on trouve dans la littérature: un premier interprète est exprimé dans une monade libre bien choisie, puis, dans un second temps, les habitants de cette monade sont traduits dans d'autres monades (monade des interaction trees; monade de spécification). Le second style, “à pas amples”, est hybride: dans une couche inférieure, on conserve le même interprète monadique, exprimé dans la monade libre; dans une couche supérieure, on raisonne à l'aide d'une sémantique opérationnelle à petits pas. J'aimerais recevoir des commentaires et suggestions du public afin de prévoir les prochaines étapes: ajout du non-déterminisme, du parallélisme, de l'état mutable, puis construction d'une logique de programmes de la famille Iris.

Combinatoire énumérative et analytique
Jeudi 30 mars 2023, 15 heures, Salle 3052
Jorge Alberto Olarte (CUNEF Universidad (Madrid)) Positivity for tropical flag varieties

In this talk we will study different positivity notions that exist for tropical flag varieties. We will start with an introduction to tropical flag varieties and the related polyhedral subdivisions. After explaining what each notion of positivity is and how do they relate to each other, I will provide equations on the Plücker coordinates for each of them. Finally, we discuss the cases where we know that these equations are sufficient.

Preuves, programmes et systèmes
Jeudi 30 mars 2023, 10 heures 30, Salle 3052 & online (Zoom link)
Romain Pascual (Université Paris-Saclay) Graph transformation for reasoning about geometric modeling operations

Topology-based geometric modeling deals with the representation of nD objects, which splits the topological description, i.e., the representation of the objects' topological cells (vertices, edges, faces, volumes, …), and the geometric information, i.e., the addition of data to the topological cells. We study the combinatorial models of generalized and oriented maps represented as attributed typed graphs subject to consistency conditions. This representation allows the study of modeling operations as graph rewriting rules. The motivation is twofold. First, we study the preservation of the model consistency through syntactic conditions statically checked on the rules. Second, we extend rules into rule schemes to abstract over the underlying topology. This formalization of modeling operations also offers guidelines for inferring operations from a representative example consisting of an initial and a target object. The inference mechanism is implemented in Jerboa, a platform for designing geometric modelers exploiting graph transformation rules.

Séminaire des doctorants
Jeudi 30 mars 2023, 16 heures, 3052 and Zoom link
Shamisa Nematollahi Submodular Maximization Problem

The study of combinatorial optimization problems with a submodular objective has attracted much attention in recent years. Such problems are important in both theory and practice because their objective functions are very general. A few examples of such functions include cuts functions of graphs and hypergraphs, rank functions of matroids, and covering functions.

Let $N = {u_1, u_2, ..., u_n}$ be a ground set of elements, A function $F : 2^{\mathcal{N}} \to R_{\geq 0}$ is submodular if for every $A \subset B \subset \mathcal{N}$ and $u \in \mathcal{N} \setminus B$, $F(A\cup\{u\})−F(A) \geq F (B \cup \{u\}) − F (B)$. Since the submodular maximization problem is NP-hard, we will discuss some important approximation algorithms of the constrained versions of the problem in both monotone and non-monotone cases.

Preuves, programmes et tout ça
Jeudi 30 mars 2023, 13 heures 30, salle 4052
Nino Salibra (Universita' Ca'Foscari Venezia) A completeness theorem for the infinitary lambda calculus

Automates
Vendredi 31 mars 2023, 14 heures, Salle 3052
Leon Bohn Non encore annoncé.

Algorithmes et complexité
Lundi 3 avril 2023, 14 heures, Salle 3052
Gabriel Le Bouder (LIP6) Memory-Optimization for Self-Stabilizing Distributed Algorithms

Self-stabilization is a suitable paradigm for distributed systems, particularly prone to transient faults. Errors such as memory or messages corruption, break of a communication link, can put the system in an inconsistent state. A protocol is self-stabilizing if, whatever the initial state of the system, it guarantees that it will return a normal behavior in finite time. Several constraints concern algorithms designed for distributed systems. Asynchrony is one emblematic example. With the development of networks of connected, autonomous devices, it also becomes crucial to design algorithms with a low energy consumption, and not requiring much in terms of resources.

One way to address these problems is to aim at reducing the size of the messages exchanged between the nodes of the network. This thesis focuses on the memory optimization of the communication for self-stabilizing distributed algorithms. We will present a negative results, proving the impossibility to solve some problems under a certain limit on the size of the exchanged messages, and a particularly efficient algorithms in terms of memory for one fundamental problem in distributed systems: the token circulation.

Vérification
Lundi 3 avril 2023, 11 heures, 1007 and Zoom link
Thomas Nowak (ENS Paris-Saclay) Reaching Consensus in Hostile Environments

Reaching consensus in a distributed system is one of the most fundamental problems studied in distributed computing. It is non-trivial due to uncertainties related to unsuccessful communication and process faults. In particular, the celebrated FLP impossibility result shows why scheduling an event via an asynchronous communication medium such as email is difficult. In this talk, I will present our recent results on exact and approximate consensus in hostile environments such as dynamic networks (e.g., due to mobility of agents) and synthetic bacterial cultures

Formath
Lundi 3 avril 2023, 14 heures, 1007
Olivier Laurent (Équipe Plume, Laboratoire de l'Informatique du Parallélisme (LIP), ENS Lyon) 1, 2, 3, Yalla: Linear Logic in Coq

We discuss the formalization of Linear Logic, through the development of the Yalla library for Coq:

https://perso.ens-lyon.fr/olivier.laurent/yalla/

The initial specification was to get a library which:

  • would provide standard results on the proof theory of Linear Logic;
  • could be reused, thus in particular able to deal with some variants of the system;
  • should be compatible with the Curry-Howard interpretation of proofs, thus faithful to their computational content.

We will describe the evolution of the project and how it matches this specification through the different versions of the library: Yalla 1, Yalla 2 (current version), Yalla 3 (future directions).

Following all previous known works, Yalla 1 defined proofs in Prop. It relies on an explicit exchange rule for dealing with the computational content of proofs. Yalla 2 corresponds to a move to Type to be able to extract computational informations from proofs. Yalla 3 will rely on a different way of approaching exchange to be able to deal with local transformations of proofs more easily.