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.

Thomas Ehrhard

28.9.2022
Thomas Ehrhard, CNRS senior researcher at IRIF, turned 60 in 2021. A meeting will take place in Paris, at the CNAM, on 29-30 September 2022 to celebrate Ehrhard’s contributions to logic and the semantics of programming languages. For more information, follow the arrow:

ICTP-EAUMP School on Mathematical Programming and Algorithms

7.9.2022
IRIF is a co-sponsor of the ICTP-EAUMP School on Mathematical Programming and Algorithms - an African Mathematical School. The 2022 summer school organized by the University of Nairobi took place at Kenya School of Government, Nairobi, Kenya 11-29 July, 2022. Three IRIF members took part of this project: Jean-Baptiste Yunès, Roberto Mantaci and Anna Vanden Wyngaerd.

Test of Time Award - LICS'22

19.9.2022
Philippe Schnoebelen (LMF), François Laroussinie (IRIF) and Nicolas Markey (IRISA), received the Test-of-Time award at the conference LICS 2022 for their research on temporal logic.

Workshop CoA 2022

2.9.2022
The 2nd Workshop Complexity and Algorithms (CoA 2022) will take place in September 26-28 2022 at Institut Henri Poincaré (IHP), Paris. Scientific program includes talks from invited speakers Marthe Bonamy (LaBRI), Carola Doerr (LIP6), Sébastien Tavenas (LAMA) and Adrian Vladu (IRIF).

Interview ICALP Leslie Ann Goldberg

11.8.2022
Leslie Ann Goldberg, invited speaker at ICALP 2022 was interviewed by La Recherche about some of the key issues she is interested in.

The EAPLS Best Paper Award 2022

8.8.2022
The European Association for Programming Languages and Systems (EAPLS) has established a Best PhD Dissertation Award in the research area of programming languages and systems. Candidates for the award must be nominated by their supervisor. Deadline for nominations : 30 August 2022.

Podcast DECODE quantum

2.9.2022
Pour son 48ème épisode, le podcast DECODE Quantum a reçu le directeur de l'IRIF Frédéric Magniez dans un entretien approfondi sur le quantique. Il est question, entre autres, d'algorithmes quantiques, de leur intérêt et de leur construction. Par ici pour écouter l'émission.

Création du prix Lovelace-Babbage

2.9.2022
L’Académie des sciences et la Société informatique de France annoncent la création d’un nouveau prix en informatique : le prix Lovelace-Babbage.


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

One world numeration seminar
Mardi 4 octobre 2022, 14 heures, Online
David Siukaev (Higher School of Economics) Exactness and Ergodicity of Certain Markovian Multidimensional Fraction Algorithms

A multidimensional continued fraction algorithm is a generalization of well-known continued fraction algorithms of small dimensions: Gauss and Euclidean. Ergodic properties of Markov MCF algorithms (ergodicity, nonsingularity, exactness, bi-measurability) affect their convergence (if the MСF algorithm is a Markov algorithm, there is a relationship between the spectral properties and its convergence).

In 2013 T. Miernowski and A. Nogueira proved that the Euclidean algorithm and the non-homogeneous Rauzy induction satisfy the intersection property and, as a consequence, are exact. At the end of the article it is stated that other non-homogeneous markovian algorithms (Selmer, Brun and Jacobi-Perron) also satisfy the intersection property and they also exact. However, there is no proof of this. In our paper this proof is obtained by using the structure of the proof of the exactness of the Euclidean algorithm with its generalization and refinement for multidimensional algorithms. We obtained technically complex proofs that differ from the proofs given in the article of T. Miernowski and A. Nogueira by the difficulties of generalization to the multidimensional case.

One world numeration seminar
Mardi 4 octobre 2022, 14 heures 30, Online
Alexandra Skripchenko (Higher School of Economics) Bruin-Troubetzkoy family of interval translation mappings: a new glance

In 2002 H. Bruin and S. Troubetzkoy described a special class of interval translation mappings on three intervals. They showed that in this class the typical ITM could be reduced to an interval exchange transformations. They also proved that generic ITM of their class that can not be reduced to IET is uniquely ergodic.

We suggest an alternative proof of the first statement and get a stronger version of the second one. It is a joint work in progress with Mauro Artigiani and Pascal Hubert.

Algorithmes et complexité
Mercredi 5 octobre 2022, 16 heures 30, Salle 3052
Daniel Szilagyi & Brandon Augustino Seminar Paris-Lehigh on Quantum Interior Point Methods

Combinatoire énumérative et analytique
Jeudi 6 octobre 2022, 14 heures, IHP
Seminaire Flajolet Jehanne Dousse, Nicolas Bonichon, Thierry Levy

Preuves, programmes et systèmes
Jeudi 6 octobre 2022, 10 heures, Salle 3052
All Hands On Deck (IRIF) Matinée de rentrée de PPS

Séminaire des doctorants
Jeudi 6 octobre 2022, 16 heures, 3052
Adrienne Lancelot (IRIF) Equivalences of Programs in the lambda calculus

In the study of programming languages, an essential point is the ability to state program equivalence, whether it is to reason abstractly or to establish that some program transformations, used typically when compiling programs, preserve the behavior of programs. The topic of this talk is the study of program equivalence for the case of programs expressed as terms of the λ-calculus, seen as a mathematical model of functional programming languages. We will survey existing program equivalences and focus on normal form bisimulations, in different variants of the lambda calculus. The lambda calculus was first introduced as a way to represent computable functions, with the Call-by-Name variant which has been extensively studied. Nowadays, functional programming languages use mostly the Call-by-Value variant (OCamL) and some the Call-by-Need variant (Haskell). In Call-by-Name, normal form bisimulations yield very satisfactory results. Unfortunately, these do not export to Call-by-Value. Part of my thesis work will be trying to find a satisfactory program equivalence in Call-by-Value.

The previous talk by Victor Arrial is a nice introduction to this talk but concepts tied to the lambda calculus (and its variants) will be re-explained. We will also need the (more generic) concept of co-induction to form program equivalences, which will be briefly explained as well.

Catégories supérieures, polygraphes et homotopie
Vendredi 7 octobre 2022, 14 heures, Salle 1007
Pierre-Louis Curien (IRIF) Une preuve élémentaire de ce que les ensembles opétopiques sont les polygraphes ``many-to-one’’

Automates
Vendredi 7 octobre 2022, 14 heures, Salle 3052
Jacques Sakarovitch (IRIF, CNRS and LTCI, Télécom Paris, IPP) The Net Automaton of a Rational Expression

In this talk, we present a new construction of a finite automaton associated with a rational (or regular) expression. It is very similar to the one of the so-called Thompson automaton, but it overcomes the failure of the extension of that construction to the case of weighted rational expressions. At the same time, it preserves all of the properties of the Thompson automaton.

This construction has two supplementary outcomes.

The first one is the reinterpretation in terms of automata of a data structure introduced by Champarnaud, Laugerotte, Ouardi, and Ziadi for the efficient computation of the position (or Glushkov) automaton of a rational expression, and which consists in a duplicated syntactic tree of the expression decorated with some additional links.

The second one supposes that this construction devised for the case of weighted expressions is brought back to the domain of Boolean expressions. It allows then to describe, in terms of automata, the construction of the Star Normal Form of an expression that was defined by Brüggemann-Klein, and also with the purpose of an efficient computation of the position automaton.

This is joint work with Sylvain Lombardy (Labri, U. Bordeaux)

Vérification
Lundi 10 octobre 2022, 11 heures, 1007 and Zoom link
Cristina Seceleanu (Mälardalen University) Reinforcement Learning for Mission Plan Synthesis of Autonomous Vehicles

Computing a mission plan for an autonomous vehicle consists of path planning and task scheduling, which are two outstanding problems existing in the design of multiple autonomous vehicles. Both problems can be solved by the use of exhaustive search techniques such as model checking and algorithmic game theory. However, model checking suffers from the infamous state-space-explosion problem that makes it inefficient at solving the problem when the number of vehicles is large, which is often the case in realistic scenarios. In this talk, we show how reinforcement learning can help model checking to overcome these limitations, such that mission plans can be synthesized for a larger number of vehicles if compared to what is feasibly handled by model checking alone. Instead of exhaustively exploring the state space, the reinforcement-learning-based method randomly samples the state space within a time frame and then uses these samples to train the vehicle models so that their behavior satisfies the requirements of tasks. Since every state of the model needs not be traversed, state-space explosion is avoided. Additionally, the method also guarantees the correctness of the synthesis results. The method is implemented in UPPAAL STRATEGO and integrated with a toolset to facilitate path planning and task scheduling in industrial use cases. We also discuss the strengths and weaknesses of using reinforcement learning for synthesizing strategies of autonomous vehicles.

One world numeration seminar
Mardi 11 octobre 2022, 14 heures, Online
Lukas Spiegelhofer (Montanuniversität Leoben) Primes as sums of Fibonacci numbers

We prove that the Zeckendorf sum-of-digits function of prime numbers, $z(p)$, is uniformly distributed in residue classes. The main ingredient that made this proof possible is the study of very sparse arithmetic subsequences of $z(n)$. In other words, we will meet the level of distribution. Our proof of this central result is based on a combination of the “Mauduit−Rivat−van der Corput method” for digital problems and an estimate of a Gowers norm related to $z(n)$. Our method of proof yields examples of substitutive sequences that are orthogonal to the Möbius function (cf. Sarnak's conjecture).

This is joint work with Michael Drmota and Clemens Müllner (TU Wien).