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.

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.

27.2.2023
One paper authored by IRIF member will be presented at STOC 2023, June 20-23, 2023 in Orlando, Florida.

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

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.

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).

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.

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.

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

Vérification
Lundi 27 mars 2023, 11 heures, 1007 and Zoom link
Lénaïg Cornanguer & Christine Largouët (IRISA Rennes) TAG: Learning Timed Automata from Logs

Event logs are often one of the main sources of information to understand the behavior of a system. While numerous approaches have extracted partial information from event logs, we aim at inferring a global model of a system from its event logs.

We consider real-time systems, which can be modeled with Timed Automata: our approach is thus a Timed Automata learner. There is a handful of related work, however, they might require a lot of parameters or produce Timed Automata that either are undeterministic or lack precision. In contrast, we propose an approach, called TAG, that requires only one parameter and learns, without any a-priori knowledge, a deterministic Timed Automaton having a good tradeoff between accuracy and automata complexity. This allows getting an interpretable and accurate global model of the considered real-time system. Experiments compare our approach to related work and demonstrate its merits.

Algorithmes et structures discrètes
Mardi 28 mars 2023, 15 heures, 3052
Lélia Blin (LIP6) Self-Stabilizing Distributed Algorithms

In the context of large-scale networks, fault tolerance is a necessity. Self-stabilization is an algorithmic approach to fault tolerance in distributed systems. Its aim is to manage processors' memory corruption due to transient failures. The efficiency of a self-stabilizing algorithm is characterized by several parameters, including (1) the time taken by the system to return to a legal configuration after an arbitrary corruption of its processors' memory, and (2) the memory space used by the processors to execute the algorithm. Minimizing memory space is motivated by many aspects, such as networks (e.g. sensor networks) with limited memory space, minimizing data exchanges between processors, and limiting information storage to use redundancy techniques. This seminar will present self-stabilization through two main classical problems: constructing spanning trees, especially those of minimum weight, and electing a leader. It will cover the links between self-stabilization and distributed decision techniques, including computing lower bounds on memory space needed to solve the aforementioned problems using self-stabilizing algorithms.

One world numeration seminar
Mardi 28 mars 2023, 14 heures, Online
Roland Zweimüller (Universität Wien) Variations on a theme of Doeblin

Starting from Doeblin's observation on the Poissonian nature of occurrences of large digits in typical continued fraction expansions, I will outline some recent work on rare events in measure preserving systems (including spatiotemporal and local limit theorems) which, in particular, allows us to refine Doeblin's statement in several ways.

(Part of this is joint work with Max Auer.)

Preuves, programmes et tout ça
Mardi 28 mars 2023, 13 heures 30, salle 3052
Fabio Massaioli (Scuola Normale Di Pisa) (Scuola Normale di Pisa) A non-trivial proof-semantics for classical sequent calculus (LK)

Cut-reduction procedures for classical sequent calculus are notoriously non-deterministic and non-confluent, both in the original formulation by Gentzen and in later reformulations. It is natural to ask whether those instances of non-confluence are superficial in nature, i.e. whether syntactically distinct normal forms of the same derivation are in fact correlated in a non-trivial way, as is the case in the intuitionistic and linear versions of sequent calculus. A famous counter-example by Lafont purports to show that the answer is negative, that is, every interpretation of derivations in LK that is invariant under classical cut-elimination must be a trivial one that identifies at least all proofs of the same sequent. A long-standing open question has then been whether it could be possible to work around Lafont's example by natural and non-trivial adjustments of the calculus and/or of cut-reduction steps, without resorting to symmetry-breaking techniques like polarization or embeddings into intuitionistic or linear logic.

Working within the propositional fragment of the context-sharing formulation of LK — where parallel logical rules permute freely — we show that the graph constructed by tracing the history of atomic formula occurrences through axiom and cut rules is invariant under arbitrary rule permutations in cut-free proofs, thus providing a canonical representation of normal-form proofs.

We then introduce a refinement of the notion of axiom-induced graph that allows extending the invariance result to proofs with cuts, although at the cost of a strong assumption on the shape of derivations. Because cut-reduction in this formulation of LK can be implemented entirely by logical rule permutations plus a pair of local rewriting steps that preserve the refined axiom graphs, the result yields a non-trivial invariant of cut-reduction.

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, 14 heures, Salle 3052
Slim Kammoun (IMT (Université de Toulouse)) Permutations et cycles

La combinatoire des statistiques (longueur de la plus longue sous-suite croissante, le nombre d'apparitions de motifs ou encore la structure en cycle d'un mot etc.) sur les permutations est généralement bien comprise, Cependant, lorsque l'on restreint l'étude à une classe de conjugaison, la question devient plus difficile. Par exemple, il reste difficile de comprendre le comportement de la longueur de la plus longue sous-suite croissante pour des permutations uniformément choisis parmi celles ayant n/3 cycles de longueur 3.

Dans cet exposé, je présente quelques résultats et plusieurs conjectures sur des phénomènes où seuls les petits cycles jouent un rôle asymptotiquement.

(Basé sur des travaux avec Natasha Blitvić, Mylène Maïda et Einar Steingrímsson.)

Combinatoire énumérative et analytique
Jeudi 30 mars 2023, 15 heures, Salle 3052

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.