L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université de Paris, 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), cinq 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.11.2021
Three accepted papers coauthored by IRIF members will be presented at POPL 2022, the main conference on programming languages and programming systems, January 16-22.

25.11.2021
Adrian Vladu's paper Faster Sparse Minimum Cost Flow by Electrical Flow Localization, jointly written with Kyriakos Axiotis and Aleksander Madry, will be presented at FOCS 2021.

25.11.2021
Giuseppe Castagna (IRIF), Mickaël Laurent (Université de Paris), Kim Nguyen (Université Paris Saclay) and Matthew Lutze (Université de Paris) will present their paper that shows a nifty way to use classic deduction rules to define a formal framework in which dynamic languages such as JavaScript can statically and precisely typed. Check the proof-of-concept implementation available at
https://typecaseunion.github.io/.

8.11.2021
On November 16th, afternoon, the pole ASD organizes an event. Short introduction talks by the four new ASD permanent members will be presented. There will also be an informal introduction of PhD students and postdocs. Schedule and details of the talks here.

4.11.2021
The Automata, Structures, and Verification (ASV) day is scheduled this year on Friday November 19th. This will be the opportunity to meet again and learn about some of the work done in our pole, in particular by the new comers. Schedule and details of the talks here.

8.11.2021
One accepted paper coauthored by Adrian Vladu (IRIF), Alexandra Peste (IST Austria), Eugenia Iofinova (Institute of Science and Technology Austria) and Dan Alistarh (IST Austria & NeuralMagic) will be presented at the 35th Conference on Neural Information Processing Systems (NeurIPS) 6-14 December 2021 : AC/DC: Alternating Compressed/DeCompressed Training of Deep Neural Networks.

29.9.2021
IRIF researchers are participating to the 30th edition of Fête de la Science. In different schools in Paris, they will be presenting workshops and games related to computer science.

25.10.2021
Tous les ans, l’IRIF accueille des élèves dans le cadre de leur stage d’observation de 3ème. Les stages proposés constituent une découverte de l’informatique et des métiers académiques correspondants, qu’ils soient au CNRS ou à l’université de Paris. Toutes les informations pour envoyer sa candidature ici.

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

Algorithmique distribuée et graphes
Mardi 30 novembre 2021, 14 heures, Salle 1007
Marco Caoduro (G-Scop) Hitting and packing squares

Let $\mathcal{S}$ be a family of (not necessarily axis parallel) squares in the plane. The \emph{transversal number} of $\mathcal{S}$, denoted by $\tau(\mathcal{S})$, is the minimum number of points needed to hit all the squares in $\mathcal{S}$, and the \emph{independence number} of $\mathcal{S}$, denoted by $\nu(\mathcal{S})$, is the maximum number of pairwise disjoint squares in $\mathcal{S}$.

Clearly, $\tau(\mathcal{S})$ is at least $\nu(\mathcal{S})$. We prove that $\tau(\mathcal{S}) \leq 10 \nu(\mathcal{S})$ and present a family where $\tau(\mathcal{S}) = 3\nu(\mathcal{S})$.

During the talk, we will sketch the proof of the main result and remark how to extend our approach to families of rectangles with \emph{bounded aspect ratios}.

This is joint work with András Sebő.

Combinatoire énumérative et analytique
Jeudi 2 décembre 2021, 14 heures, Salle 1007
Ariane Carrance (CMAP, Ecole Polytechnique) Énumération de nouvelles conditions de bord pour les cartes bicolorées

Les cartes bicolorées à bord apparaissent dans de nombreux contextes : elles sont notamment un cas particulier du modèle d'Ising. Ainsi, dans le cas d'un bord monochromatique, très naturel pour le modèle d'Ising, les cartes bicolorées ont été énumérées par plusieurs méthodes, tant analytiques que bijectives. Cependant, pour l'étude de modèles de cartes aléatoires, il est plus naturel de considérer d'autres conditions de bord, comme la condition dite alternante. Dans cet exposé, je présenterai les résultats et les principaux arguments d'un travail en commun avec Jérémie Bouttier, où nous utilisons des outils de combinatoire analytique pour énumérer les cartes bicolorées à bord alternant. Les résultats intermédiaires que je présenterai feront aussi apparaître d'autres motivations pour s'intéresser à ces conditions de bord.

Preuves, programmes et systèmes
Jeudi 2 décembre 2021, 10 heures 30, Virtual room at link (any password works)
Sylvain Boulmé (Verimag) Formally Verified Assembly Optimizations by Symbolic Execution.

Necula (PLDI'2000) and Tristan, Gouvereau, Morrisett (PLDI'2011) established that symbolic execution combined with rewriting is effective in validating the code produced by state-of-the-art compilers applying various optimizations. In the meantime, Tristan and Leroy (POPL'2008) used formally-verified symbolic execution to certify the schedules produced by untrusted oracles – optimizing pipeline usage – within the CompCert compiler. Alas, their formally-verified checker had exponential complexity and was thus never integrated into mainline CompCert.

With Cyril Six and David Monniaux, we solved this performance issue with formally verified hash-consing within the symbolic execution. And we successfully applied this technique to implement within CompCert effective optimizations targeting superscalar (or VLIW) in-order processors.

The talk will actually start by briefly introducing a sound Foreign Function Interface for embedding OCaml oracles within Coq. Hence, it will explain how we used it in this application.

Analyse et conception de systèmes
Jeudi 2 décembre 2021, 14 heures, salle 15-16 101 (campus Jussieu)
Raphael Monat (APR/LIP6/Sorbonne Université) A Modern Compiler for the French Tax Code

Gâteau de l'IRIF
Jeudi 2 décembre 2021, 16 heures 30, 3052
Pierre Meyer, Daniel Szilagyi Gâteau de l'IRIF

IRIF CakeTM is an amazing opportunity to meet people while simultaneously eating cakes baked by your fellow colleagues! Join us every Thursday, at 5pm, in front of room 3052 (Sophie Germain 3rd floor) for a weekly feast. You can also express your cooking skills and volunteer to bake a cake by sending an email to cake@irif.fr.

Catégories supérieures, polygraphes et homotopie
Vendredi 3 décembre 2021, 14 heures, Salle 1007
Guillaume Laplante-Anfossi (Université Sorbonne Paris-Nord) La diagonale des opéraèdres

La diagonale ensembliste d’un polytope a le défaut rédhibitoire de ne pas être cellulaire: son image n’est pas une union de cellules. Notre but sera ici de développer une théorie générale, basée sur la méthode introduite par N. Masuda, H. Thomas, A. Tonks et B. Vallette, afin de comprendre et de manipuler les approximations cellulaires de la diagonale d’un polytope quelconque. Cette théorie nous permettra d’attaquer le problème de l’approximation cellulaire de la diagonale des opéraèdres, une famille de polytopes allant des associaèdres aux permutoèdres, et qui code les opérades à homotopie près. Nous obtiendrons ainsi une formule explicite pour le produit tensoriel de deux telles opérades, aux propriétés combinatoires intéressantes.

Référence: https://arxiv.org/abs/2110.14062

Automates
Vendredi 3 décembre 2021, 14 heures 30, Salle 3052 (Online)
Jan Otop (University of Wrocław) Active learning automata with syntactic queries

Regular languages can be actively learned with membership and equivalence queries in polynomial time. The learning algorithm, called the L^* algorithm, constructs iteratively the right congruence relation of a given regular language L, and returns the minimal DFA recognizing L. The L^* algorithm has been adapted to various types of automata: tree automata, weighted automata, nominal automata. However, an extension to infinite-word automata has been elusive. In this talk, I will present an extension of the active learning framework, in which the algorithm can ask syntactic queries about the automaton representing a given infinite-word language.

First, I will discuss why extending L^*, which asks only semantic queries, to infinite-words languages is difficult. Next, I will present an alternative approach; instead of learning some automaton for a hidden language, we assume that there is a hidden automaton and the algorithm is supposed to learn an equivalent automaton. In this approach, the learning algorithm is allowed to ask standard semantic queries (membership and equivalence) and loop-index queries regarding the structure of the hidden automaton. These queries do not reveal the full structure of the automaton and hence do not trivialize the learning task.

In the extended framework, there are polynomial-time learning algorithms for various types of infinite-word automata: deterministic Buechi automata, LimSup-automata, deterministic parity automata and limit-average automata.

Finally, the idea to incorporate syntactic queries can be adapted to the pushdown framework; I will briefly discuss the learning algorithm for deterministic visibly pushdown automata.

Graph Transformation Theory and Applications
Vendredi 3 décembre 2021, 15 heures, online
Daniel Strüber (Department of Computer Science and Engineering, Chalmers University of Technology, University of Gothenburg, Sweden) Supporting Software Variability with Graph Transformations

Software systems and the artifacts they consist of often exist in many different variants. When creating new variants, developers typically rely on the “clone and own” strategy of copying and modifying existing variants, a simple and intuitive approach with significant long-term disadvantages. In this talk, I present a line of work on supporting variants in software engineering by explicitly addressing variability as a feature in graph transformations. I focus on three transformation scenarios: one where the input graph has variability (representing the established notion of a software product line), one where rules have variability (leading to variability-based rules), and a combination of the first two scenarios. Each scenario is supported with formal constructions, efficient transformation algorithms, and tool support. Our work shows that a systematic way of supporting variability in transformations can improve the maintainability and the performance of a software system.