Institut de Recherche en Informatique Fondamentale (IRIF)


image/svg+xml

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.

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

visiteur-serge-massar

2.12.2021
IRIF is very pleased to host for one month Serge Massar, Professor at the Université libre de Bruxelles (ULB) as part of the FSMP Distinguished Professor Fellowship. Serge Massar is the director of the Laboratoire d'Information Quantique (LIQ), of the Physics Department, Science Faculty, ULB. His research interests are quantum information theory, experimental quantum and non linear optics, machine learning.

conference-75ans-fabrice-kordon

1.12.2021
Prochaine conférence dans le cadre des 75 ans d’informatique : L’informatique dans le 7ème art : fiction ou réalité ? Rendez-vous avec Fabrice Kordon le jeudi 9 décembre-18h00 sur le campus Pierre et Marie Curie de Sorbonne Université (tour 25.26, 1er étage – salle 105).

Accepted papers POPL 2022

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.

hpcqs project

2.12.2021
We are excited to be part of the “High-Performance Computer and Quantum Simulator hybrid” (HPCQS) aiming at creating a world-class supercomputing ecosystem. Learn more about the project here.

Portrait Matej Stehlik

29.11.2021
IRIF has the great pleasure to welcome a new professor in computer science at Université de Paris: Matěj Stehlík, an expert in graph theory. Learn more about him and his work here.

Accepted paper FOCS 2021

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.

Journée du pôle ASD 2021

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.


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

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, 17 heures, 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.

Zoom meeting registration link

YouTube live stream

Vérification
Lundi 6 décembre 2021, 11 heures, 1007 and Zoom link
Alessio Mansutti (University of Oxford) Efficient complementation of semilinear sets and the VC dimension of Presburger arithmetic

We discuss the issue of deciding the first-order theory of integer linear arithmetic, also known as Presburger arithmetic. Whereas optimal decision procedures based on either quantifier-elimination or automata constructions are known for this theory, the current procedures based on manipulating semilinear sets (i.e. sets that geometrically characterise the solutions of a formula) are extremely inefficient. We address this issue by deriving a new algorithm for computing the complement of a semilinear set, which in particular is optimal for nested complementations. Alongside solving the aforementioned discrepancy between semilinear-based algorithms and other types of procedures, this result allows us to characterise the Vapnik-Chervonenkis dimension of Presburger arithmetic, which is found to be doubly-exponential. The results in this talk are joint work with Christoph Haase and Dmitry Chistikov.

Algorithmes et complexité
Mardi 7 décembre 2021, 11 heures, Salle 1007
Bruce Kapron (Computer Science Department, University of Victoria) Type-two feasibility via bounded query revision

The problem of generalizing the notion of polynomial time to a type-two setting, where inputs include not only finitary data, e.g., numbers or strings of symbols, but also functions on such data, was first posed by Constable in 1973. Mehlhorn subsequently proposed a solution, based on a generalization Cobham's scheme-based approach which uses limited recursion on notation. The resulting class was shown to be robust with respect to oracle Turing machine (OTM) computation, but the problem of providing a purely machine-based characterization remained open for almost two decades, when Kapron and Cook gave a solution using notions of function length and second-order polynomials. While a natural generalization of the usual notion of poly-time, this characterization still had some shortcomings, as function length is itself not a feasible notion. A charaterization using ordinary polynomials remained an elusive goal.

Recently, we have provided several such characterizations. The underlying idea is to bound run time in terms of an ordinary polynomial in the largest answer returned by an oracle, while imposing a constant upper bound on the number of times an oracle query (answer) may exceed all previous ones in size. The resulting classes are contained in Mehlhorn's class, and when closed under composition are in fact equivalent.

In this talk we will present these recent results and follow-up work involving new scheme-based characterizations of Mehlhorn's class, as well as a recent characterization using a tier-based type system for a simple imperative programming language with oracle calls.

(Joint work with F. Steinberg, and with E. Hainry, J.-Y. Marion, and R. Pechoux.)

Algorithmes et complexité
Mardi 7 décembre 2021, 14 heures, 3052
Daniel Szilagyi Introduction to convexity - optimization and sampling

In this talk we present some basic notions of convexity, from a quantum-algorithmic point of view. The talk will consist of two parts. We first warm-up by introducing some classical first- and second-order methods for convex optimization. Then, we move on to more structured convex problems, introduce linear programming and the basic ideas of interior-point methods. We mention some quantum algorithms for LPs and SDPs. In the second part of the talk we discuss sampling, and in particular its applications to estimating volumes of polytopes. We present the basic classical sampling algorithms (ball walk and hit-and-run), and the general framework for applying these algorithms to volume estimation. We conclude by discussing the opportunities for quantum speedups - in particular, we present a high-level overview of the work by Chakrabarti, Childs, Hung, Li, Wang and Wu from 2019.

One world numeration seminar
Mardi 7 décembre 2021, 14 heures 30, Online
Jamie Walton (University of Nottingham) Non encore annoncé.

Théorie des types et réalisabilité
Mercredi 8 décembre 2021, 14 heures, Salle 1007
Federico Olimpieri (Université de Leeds) Categorifying Intersection Types

We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction.

Combinatoire énumérative et analytique
Jeudi 9 décembre 2021, 14 heures, Salle 1007
Harriet Walsh (IRIF, Université de Paris) Non encore annoncé.

Gâteau de l'IRIF
Jeudi 9 décembre 2021, 17 heures, 3052
Clément Ducros, Sander Gribling 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.