Institut de Recherche en Informatique Fondamentale (IRIF)


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.

Conference Highlights 2022

The 2022 edition of Highlights will happen from June 28th to July 1st, 2022, in Paris, France. The conference will be hosted by Université Paris Cité, and happen on the site of Grands Moulins. To register, please fill in the registration form. If you wish to watch Highlights remotely, please fill in the online registration form. Online attendance is free.

Four papers coauthored by IRIF members will be presented at the conference PODC'22, the main conference on distributed computing, this summer.

Institut Universitaire de France

IRIF is proud to announce that Olivier Carton, professor of Université Paris Cité and researcher at IRIF, was appointed senior member of IUF.

Two papers coauthored by IRIF members will be presented at the conference ISSAC'22, the main conference on symbolic and algebraic computation , this summer.

IRIF is co-organizing a Workshop on Differentiable Programming, June 29-30, Université Paris Cité.

Four papers coauthored by IRIF members will be presented at the conference TYPES'22, the main conference on type theory, this summer.

IRIF is co-organizing a Workshop Labyrinth of Combinatorics in memory of Pierre Rosenstiehl, June 15-17, Université Paris Cité

ICALP 2022 Accepted papers

3 papers coauthored by IRIF members will be presented at ICALP 2022, July 4-8 in Paris, campus Grands Moulins of Université Paris Cité. Complete list of accepted papers here.

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

Nombre limité d'évènements durant les vacances d'été.

Analyse et conception de systèmes
Vendredi 1 juillet 2022, 10 heures 30, Salle 3052
Jean-Baptiste Tristan (Boston College) Probabilistic Programming and Molecular Optimization (Zoom link)

The energy of a system of atoms is approximately a function of the position of the nuclei. This function is called the potential energy surface (PES). Knowledge of the PES is fundamental in ab-initio sciences but unfortunately, it cannot be computed in closed form. As a result, an important problem is that of exploring the PES to discover important features, such as local minima.

In this talk, I will introduce an experimental probabilistic programming language designed to facilitate the exploration of PES. In this language, the semantics of a program is a probability distribution over PES. The objective of the compiler is to generate an optimizer that combines solvers from machine learning and quantum chemistry to discover local minima of the PES. While much of this language and compiler is routine, we will see that the principle of conservation of energy brings about genuinely interesting compilation problems.

Lundi 4 juillet 2022, 11 heures, 1007 and Zoom link
Radosław Piórkowski (Universit of Warsaw) Synthesis games over infinite alphabets

We define timed/register synthesis games as a generalisation of the classical Büchi-Landweber games.

For such games, the problem of synthesising a winning controller turns out to be decidable when we bound the number of clocks/registers the Controller player has at his disposal, and undecidable otherwise.

I will prove the decidability result mentioned above in the setting of register automata, which is a generalisation of the Büchi-Landweber theorem. Additionally, I will mention adaptations needed to move to the timed setting.

Time permitting, I will mention an application of these games to a problem of deterministic separability of NTA/NRA.

One world numeration seminar
Mardi 5 juillet 2022, 14 heures 30, Online
Charlene Kalle (Universiteit Leiden) Random Lüroth expansions

Since the introduction of Lüroth expansions by Lüroth in his paper from 1883 many results have appeared on their approximation properties. In 1990 Kalpazidou, Knopfmacher and Knopfmacher introduced alternating Lüroth expansions and studied their properties. A comparison between the two and other comparable number systems was then given by Barrionuevo, Burton, Dajani and Kraaikamp in 1996. In this talk we introduce a family of random dynamical systems that produce many Lüroth type expansions at once. Topics that we consider are periodic expansions, universal expansions, speed of convergence and approximation coefficients. This talk is based on joint work with Marta Maggioni.

Théorie des types et réalisabilité
Mercredi 6 juillet 2022, 14 heures, Salle 1007
James Lipton (Wesleyan Univ., USA) CUT ELIMINATION in Higher-Order with (HO) constraints

We will present a system of Intensional Higher-Order Intuitionistic Logic with Higher-Order Saraswat Constraints, hoI(C). The Logic and its variants were developed by Artalejo, Nieva, Leach (Madrid), and subsequently by Lipton, Nieva and Hermant, the original aim being to add constraints to a lambda-Prolog style language.

If constraints are unrestricted, cut-elimination is easily shown to fail, because of the way the system handles equality rules. Our work studies conditions on the constraint system C that guarantee cut-elimination. The techniques used are based on Takahashi, Prawitz ande Andrews' work in classical type theory, Lipton and DeMarco for intuitionistic type theory, with ideas developed by Hermant for Logique Modulo, Hermant and Lipton for Logic with sequent axioms, as well as cut-elimination techniques due to Okada and Maehara.

We will briefly discuss Kripke and HA semantics for these calculi, with some remarks on fibrational semantics developed by the speaker with Gianluca Amato (Pescara, Italy) if time permits!

This will be a blackboard talk (with maybe a few slides) and will include work in progress!

Analyse et conception de systèmes
Vendredi 8 juillet 2022, 10 heures 30, Salle 1007
Ada Vienot (IRIF) A reactive operational semantics for a lambda-calculus with time warps

Many computer systems are reactive: they execute in continuous interaction with their environment. From the perspective of functional programming, reactive systems can be modeled and programmed as stream functions. Several lines of research have exploited this point of view. Works based on Nakano’s guarded recursion use type-theoretical modalities to guarantee productivity. Works based on synchronous programming use more specialized methods but guarantee incremental processing of stream fragments. In this paper, we contribute to a recent synthesis between the two approaches by describing how a language with a family of type-theoretical modalities can be given an incremental semantics in the synchronous style. We prove that this semantics coincides with a more usual big-step semantics.

Lundi 11 juillet 2022, 11 heures, 3052 and Zoom link
Jaco Van De Pol (Aarhus University) Parallel SCC Detection for Model Checking – Model Checking for Parallel SCC detection

I will introduce a multicore algorithm for the parallel detection of Strongly Connected Components. The algorithm uses a concurrent Union-Find forest to share partial SCCs. As a consequence, we get parallel speedup even if the graph consists of a single SCC. The algorithm works on-the-fly, so it is useful for parallel LTL model checking.

Since parallel graph algorithms are error prone, and this one is used in verification tools, we would like to verify it. We will report a first step, modeling the algorithm in TLA+ and model checking it for instances with a few workers and small graphs.

Algorithmes et complexité
Mardi 12 juillet 2022, 10 heures, Salle 3052
Seeun William Umboh (The University of Sydney) Online Weighted Cardinality Joint Replenishment Problem with Delay

We study a generalization of the classic Online Joint Replenishment Problem (JRP) with Delays that we call the Online Weighted Cardinality JRP with Delays. The JRP is an extensively studied inventory management problem wherein requests for different item types arrive at various points in time. A request is served by ordering its corresponding item type. The cost of serving a set of requests depends on the item types ordered. Furthermore, each request incurs a delay penalty while it is left unserved. The objective is to minimise the total service and delay costs. In the Weighted Cardinality JRP, each item type has a positive weight and the cost of ordering is a non-decreasing, concave function of the total weight of the item types ordered. This problem was first considered in the offline setting by Cheung et al.~(2015) but nothing is known in the online setting. Our main result is a deterministic, constant competitive algorithm for this problem.

Algorithmes et complexité
Mardi 12 juillet 2022, 11 heures, Salle 3052
Kheeran Naidu (University of Bristol) Space Optimal Vertex Cover in Dynamic Streams (with an overview of graph streaming)

With the world as connected as ever and data being created at an unprecedented rate, there has been an increasing need for algorithms that efficiently process massive graphs. Graph streaming is one such memory efficient setting where the edges of a graph are presented as a sequence of edges and an algorithm's goal is to store a sublinear number of edges needed to solve a graph problem exactly or approximately. In particular, this talk discusses the insertion-only, dynamic (or insertion-deletion) and sliding window graph streaming models of computation, highlighting the well-studied maximum matching and sister minimum vertex cover problems, and focusing on a recent space optimal (up to constant factors) algorithm for minimum vertex cover in the dynamic graph streaming model.

One world numeration seminar
Mardi 12 juillet 2022, 14 heures 30, Online
Ruofan Li (South China University of Technology) Rational numbers in ×b-invariant sets

Let $b \ge 2$ be an integer and $S$ be a finite non-empty set of primes not containing divisors of $b$. For any $\times b$-invariant, non-dense subset $A$ of $[0,1)$, we prove the finiteness of rational numbers in $A$ whose denominators can only be divided by primes in $S$. A quantitative result on the largest prime divisors of the denominators of rational numbers in $A$ is also obtained. This is joint work with Bing Li and Yufeng Wu.