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.

Postdoc position ANR-VeSyAM

27.1.2023
A full-time research associates position is available to work on the ​VeSyAm research project. The position will start in July 2023. Deadline to apply: 12 noon on 15 Feb 2023. Further information in the job description.

Internship proposal at LS2N and IRIF

13.1.2023
Internship proposal for Masters student in computer science at LS2N and IRIF in Real-time analysis and verification of ROS2 robotic applications. To apply, please refer to the internship description.

Découpage électoral des circonscriptions législatives en France : Déséquilibres démographiques et contraintes territoriales

16.1.2023
Claire Mathieu and 8 other authors co-authored the article "Découpage électoral des circonscriptions législatives en France : Déséquilibres démographiques et contraintes territoriales" about a new perspective for understanding electoral maps, using computational social science to study the criteria which shape how electoral districts are drawn up in France.

Emission Arrêt sur Images

25.1.2023
Claire Mathieu, membre de l’IRIF et spécialiste des algorithmes, est intervenue à l’émission Arrêt sur Images autour du ChatGPT. Comment cette IA construit-elle ses textes ? Pourquoi parvient-elle à couvrir à peu près n’importe quel sujet ?

Prix de thèse de la chancellerie des Universités de Paris

12.12.2022
Jonas Landman, former PhD student at IRIF, is the 2022 winner of a thesis Prize from Chancellerie des Universités de Paris. His thesis “Quantum Algorithms for Unsupervised Machine Learning and Neural Networks” was awarded in the All Specialties Science Prize Category.

Portrait Marie Albenque

14.12.2022
We are very pleased to welcome Marie Albenque, Senior Research Scientist at CNRS. Learn more about her and her work in this written interview.

Workshop LAFI'23

11.1.2023
LAFI'23, a workshop affiliated to POPL’23 about Languages for Inference, will be held on January 15, 2023, as a bi-located event in Boston and at Université Paris Cité. The Paris antenna will take place in salle Leduc, at the first floor of Saints-Pères building, 45 rue des Saints-Pères, 75006 Paris, from 3pm to 9:30pm Paris time. The The talks of V. Blanchi, G. Caylak, M. Pagani (IRIF), F. Zaiser will happen physically in Paris. Registration is mandatory.

Ahmed Bouajjani Honorary Doctor

14.12.2022
Ahmed Bouajjani (IRIF) figures among the nine new honorary doctors appointed at Faculty of Science and Technology of Uppsala University. His research focuses on verification, specification and semantics for parallel and distributed programs and computer systems.


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

Combinatoire énumérative et analytique
Jeudi 9 février 2023, 14 heures, Salle 3052 et zoom
Groupe De Lecture - Philippe Biane (CNRS LIGM) A walk through the symmetric group: non-crossing partitions, Tamari lattices, parking functions and Hurwitz graphs

I will cover basic material on non-crossing partitions, the permutahedron and the Tamari lattice, then I will show how these structures play a prominent role in the description of the Hurwitz graph, which is a graph built on the maximal chains in the lattice of non-crossing partitions (or equivalently on parking functions). In particular we will see that the projection from the permutahedron to the Tamari lattice extends to a projection from parking functions to non-crossing trees. I will try to say simple things about simple objects

The slides are in english but, depending on the audience, I will give the talk in english or in french

Preuves, programmes et systèmes
Jeudi 9 février 2023, 10 heures 30, Salle 3052 & online (Zoom link)
Clément Blaudeau (INRIA Paris, CAMBIUM Project-Team) Retrofitting OCaml modules

ML modules are offer large-scale notions of composition and modularity. Provided as an additional layer on top of the core language, they have proven both vital to the working OCaml and SML programmers, and inspiring to other use-cases and languages. Unfortunately, their meta-theory remains difficult to comprehend, and more recent extensions (abstract signatures, module aliases) lack a complete formalization. Building on a previous translation from ML modules to Fω, we propose a new comprehensive description of a significant subset of OCaml modules, including both applicative and generative functors and the proposed feature of transparent ascription. By exploring the translations both to and from Fω, we provide a complete description of the signature avoidance issue, as well as insights on the limitations and benefits of the path-based approach of OCaml type-sharing.

Analyse et conception de systèmes
Jeudi 9 février 2023, 14 heures, salle séminaires au plateau SCAI (Esclangon, 1er étage, campus Jussieu)
Catarina Urban (Inria) Interpretability-Aware Verification of Machine Learning Software

Machine learning (ML) software is increasingly being employed in high stakes or sensitive applications. This poses important safety, privacy, and non-discrimination challenges. As a consequence, research in ML verification rapidly gained popularity and demand for interpretable ML models is more and more pronounced. Interpretability and verification are typically seen as orthogonal concerns. Research in ML interpretability is mainly carried out in the ML community, while research in ML verification is mostly carried out in the formal methods community, without much communication and exchanges between these research areas. In this talk, we advocate for closing this gap by presenting our recent and ongoing work on interpretability-aware verification of ML software. On the one hand, we show how verification can aid interpretability by providing a new feature importance measure for support vector machines. On the other hand, we discuss how interpretability can guide verification by proposing a new saliency-guided robustness verification problem for deep neural networks. We conclude with plans and perspectives on future work.

Commission IRIF et environnement
Jeudi 9 février 2023, 16 heures, 3052
La Commission Première réunion de la commission IRIF et environnement

Présentation des objectifs et de l'organisation de la commission.

Tous les membres du laboratoire sont conviés, à écouter, participer, proposer, et éventuellement s'engager.

Catégories supérieures, polygraphes et homotopie
Vendredi 10 février 2023, 14 heures, Salle 1007
El Mehdi Cherradi (IRIF) La structure de modèle “smothering” sur Cat et les semidérivateurs comme (oo,1)-catégories

La notion de foncteur “smothering” (étouffant en français …), introduite par Riehl et Verity, apparaît fréquemment en homotopie, par exemple le foncteur de comparaison entre la catégorie homotopique de $Ho(C^\rightarrow)$ et la catégorie de flèche $Ho(C)^\rightarrow$ pour toute quasicatégorie $C$. Une légère variation de cette notion se trouve définir la classe d'équivalence faible d'une localisation de Bousfield à droite de la structure de modèle naturelle sur Cat. Le but de l'exposé est d'illustrer l'importance de cette structure en définissant une structure de modèle induite sur la catégorie des semidérivateurs montrant que ces derniers modélisent les $(\infty,1)$-catégories.

Automates
Vendredi 10 février 2023, 14 heures, Salle 3052
Uli Fahrenberg An invitation to higher-dimensional automata theory

I will give a gentle introduction to higher-dimensional automata (HDAs) and their language theory. HDAs have been introduced some 30 years ago as a model for non-interleaving concurrency which generalizes, for example, Petri nets while retaining some automata-theoretic intuition. They have been studied mostly for their operational and geometric aspects and are one of the original motivations for directed algebraic topology. In a series of papers we have recently started to work on the language theory of HDAs: we have introduced languages of HDAs as weak sets of interval pomsets with interfaces and shown that HDAs satisfy Kleene and Myhill-Nerode type theorems. The picture which emerges is that, even though things can sometimes get hairy in proofs, HDAs have a rather pleasant language theory, a fact which should be useful in the theory of non-interleaving concurrency and its applications. Joint work with Christian Johansen, Georg Struth, and Krzysztof Ziemiański

Vérification
Lundi 13 février 2023, 11 heures, 1007 and Zoom link
Rémi Morvan (LaBRI) Universal algorithms for parity games and nested fixpoints

The problem of solving parity games, or equivalently model-checking for mu-calculus, is known to be both in NP and co-NP: hence, it is widely believed that they are not NP-complete (nor coNP-complete). Yet, for 30 years, we failed to find a polynomial-time algorithm solving them, despite active research on the topic.

The first quasi-polynomial algorithm was found in 2017. Soon after, McNaughton-Zielonka algorithm (an exponential-time recursive algorithm, which is arguably one of the simplest algorithm for solving parity games, and the most effective in practice) was tweaked, first by Parys and then by Lehtinen, Schewe and Wojtczak, to run in quasipolynomial time. In some sense, these algorithms forces McNaughton-Zielonka algorithm to skip enough recursive calls as to run in quasipolynomial time, but not too much so that the output remains correct. We introduce a meta-algorithm that solves parity games, parametrized by trees, which will precisely guide the recursive call made by the algorithm, and show that the output is correct when the trees satisfy some combinatorial property called universality, introduced by Fijalkow and co-authors. McNaughton-Zielonka algorithm and variations can all three be seen as an instantiation of this meta-algorithm on particular classes of universal trees.

I will also emphasize and reformulate these ideas in the slightly more general context of nested fixpoints over finite lattices, and show that these algorithms can be turned into symbolic algorithm that only uses logarithmic symbolic space. The talk is mainly based on a joint work with Marcin Jurdziński and K. S. Thejaswini. The results were proven independently by André Arnold, Damian Niwiński and Paweł Parys, for nested fixpoints.

Preuves, programmes et systèmes
Mardi 14 février 2023, 11 heures, Salle 3052 & online (Zoom link)
Benoît Valiron (CentraleSupélec) Complete Equational Theories for Linear Optical and Quantum Circuits

In this talk, we introduce two complete equational theories: one for linear optical circuits and one for quantum circuits. More precisely, in both cases we introduce a set of circuit equations that we prove to be sound and complete: two circuits represent the same quantum evolution if and only if they can be transformed one into the other using the equations.

We shall first present our proposed equational theory for linear optical circuits. We shall then discuss how the semantics of both kind of circuits differ, and how to relate them using controlled-gates. The discussion will drive is to the completeness result for quantum circuits, based on the one for linear optical circuits.

Algorithmes et complexité
Mardi 14 février 2023, 11 heures, Salle 3052
Benoît Valiron (LMF, CentraleSupélec) Complete Equational Theories for Linear Optical and Quantum Circuits

In this talk, we introduce two complete equational theories: one for linear optical circuits and one for quantum circuits. More precisely, in both cases we introduce a set of circuit equations that we prove to be sound and complete: two circuits represent the same quantum evolution if and only if they can be transformed one into the other using the equations.

We shall first present our proposed equational theory for linear optical circuits. We shall then discuss how the semantics of both kind of circuits differ, and how to relate them using controlled-gates. The discussion will drive is to the completeness result for quantum circuits, based on the one for linear optical circuits.

One world numeration seminar
Mardi 14 février 2023, 14 heures, Online
Yining Hu (Huazhong University of Science and Technology) Algebraic automatic continued fractions in characteristic 2

We present two families of automatic sequences that define algebraic continued fractions in characteristic $2$. The period-doubling sequence belongs to the first family $\mathcal{P}$; and its sum modulo $2$, the Thue-Morse sequence, belongs to the second family $\mathcal{G}$. The family $\mathcal{G}$ contains all the iterated sums of sequences from the $\mathcal{P}$ and more.