Institut de Recherche en Informatique Fondamentale (IRIF)

CNRS

Université Paris Cité

IRIF is a research laboratory of CNRS and Université Paris Cité, also hosting one Inria project-team.

The research conducted at IRIF is based on the study and understanding of the foundations of all computer science, in order to provide innovative solutions to the current and future challenges of digital sciences.

IRIF hosts about 200 people. Seven of its members have been distinguished by the European Research Council (ERC), six are members of the Institut Universitaire de France IUF), two are members of the Academia Europæa, and one is member of Académie des sciences.

Follow us on Twitter/X, LinkedIn and Mastodon for our latest news:

LinkedIn Twitter/X Mastodon

podcastrechercheclairemathieufc.jpg

19.3.2024
After being increased in September 2023, the budget allocated to the french Higher Education and Research is finally reduced by 904 million euros. The podcast “La Science, CQFD” by France Culture wondered how French research is faring and what direction it is taking. Claire Mathieu, research director at CNRS at IRIF, intervenes.

12.3.2024
Hugo Herbelin, research director at Inria in IRIF, is organizing the next french speaking Horizon Maths day on the topic: Mathematical Proof and Software Safety. It will take place on Wednesday, March 27, 2024, from 9 a.m. to 6 p.m. at the Henri Poincaré Institute (5 rue Pierre et Marie Curie, Paris 5th), Hermite amphitheater. Free but mandatory registration:

15.3.2024
The 2nd french speaking conference «On éteint, on réfléchit, on discute» organized at Université Paris Cité by François Laroussinie focuses on «Les communs numériques» (“Digital Commons”). Serge Abiteboul and Valerie Peugeot are the invited speakers. It will be held on March 19, 2024, from 4pm to 6pm. This is a free of charge event.

30.1.2024
How to design algorithms to analyze protocols in electronic voting ? How to define mathematically vote secrecy ? What is at stake ? Read the interview Véronique Cortier granted us before her distinguished talk on 7 February, 2024.

31.1.2024
What kind of research policy? In an article for the french newspaper l'Humanité, Claire Mathieu explains the importance of research for France and the urgent need to make the field more attractive again, at the risk of driving away young researchers.

5.2.2024
Join IRIF as Financial Management Manager! As part of an administrative team supervised by the Administrative Manager and consisting of 5 staff (including 3 managers under your responsibility), you will organise tasks relating to the preparation, implementation and monitoring of financial operations. Application deadline: Friday 23 February 2024. | Planned start date: 1 March 2024

imdea.jpg

24.1.2024
On 23 January, Loïc Peyrot, a doctoral student at the IRIF, was invited to speak on the subject of “Record polymorphism for set-theoretic types” at the IMDEA Software Institute.

29.1.2024
One full professor (professeur des universités) and two associate professor (maître de conference) positions will open at IRIF. Fluency in French is mandatory for these positions. The application deadline is March the 6th 2024 (16h00 - Paris time)

(These news are displayed using a randomized-priority ranking.)

Enumerative and analytic combinatorics
Tuesday March 19, 2024, 11AM, Salle 3058
Victor Nador (IMPAN Krakow) Modèles de tenseurs aléatoires et double limite d’échelle

Le développement perturbatif en graphe de Feynman des matrices Hermitiennes aléatoires s’exprime comme la série génératrice de cartes pondérées, et ce développement est topologique dans la limite des matrices de grande taille N. Les modèles de matrices aléatoires fournissent ainsi un cadre simplifié pour étudier les propriétés d’une théorie de gravité quantique en deux dimensions. Les modèles de tenseurs aléatoires sont une extension de cette idée en dimensions supérieures. Dans cet exposé, après une présentation du cas matriciel, je présenterai les principales propriétés du développement de grande taille pour les tenseurs aléatoires. Je montrerai également comment une méthode combinatoire -la décomposition en schémas- nous permet d’accéder à la double limite d’échelle de ces modèles malgré la méconnaissance de la plupart des ordres du développement en 1/N.

Algorithms and complexity
Tuesday March 19, 2024, 11AM, Salle 3052
Joon Lee (EPFL) The Sparse Parity Matrix

The last decade witnessed several pivotal results on random inference problems where the aim is to learn a hidden ground truth from indirect randomised observations; much of this research has been guided by statistical physics intuition.  Prominent examples include the stochastic block model, low-density parity check codes or compressed sensing.  In all random inference problems studied so far the posterior distribution of the ground truth given the observations appears to enjoy a key property called “strong replica symmetry”.  This means that the overlap of the posterior distribution with the ground truth (basically the number of bits that can be learned correctly) concentrates on a deterministic value. Whether this is generally true has been an open question.  In this paper we discover an example of an inference problem based on a very simple random matrix over F2 that fails to exhibit strong replica symmetry.  Beyond its impact on random inference problems, the random matrix model, reminiscent of the binomial Erdos-Renyi random graph, gives rise to a natural random constraint satisfaction problem related to the intensely studied random k-XORSAT problem.

Distributed algorithms and graphs
Tuesday March 19, 2024, 3:15PM, Room 3052
Michel Habib On some recursive linear time algorithms on graphs

joint work with Derek Corneil (Toronto), Marc Tedder (Toronto), Christophe Paul (Montpellier)

We present a general scheme to design linear time recursive algorithm on graphs. As an application I will detail an algorithm that computes the modular decomposition tree of an undirected graph in linear time. This algorithm was presented at Icalp 08 (12 pages) and the full is version (42 pages) is now available at https://arxiv.org/abs/0710.3901

To this aim I will present the combinatorial structures needed. In particular the linear time behavior heavily relies on the recursive structure of a nice graph search : Lexicographic Breadth First Search (LexBFS).

Habilitation defences
Wednesday March 20, 2024, 10AM, Amphithéâtre Turing, bâtiment Sophie Germain
Geoffroy Couteau (IRIF) Correlated Pseudorandomness in Secure Computation

The focus of this habilitation thesis is on secure computation, an area of cryptography that lets multiple parties distributively compute a function on their private data. After providing a high-level introduction to my work in cryptography, the manuscript provides a gentle introduction to secret-sharing-based secure computation, which is aimed at a general audience. Then, the last chapter covers some of my contributions to secure computation through the introduction and construction of pseudorandom correlation generators (PCG), a cryptographic primitive that enables considerable efficiency improvements for a wide variety of secure computation protocols. I provide a step-by-step introduction to the notion of PCG and its security properties, outline the challenges in building them, and present a general framework for constructing PCGs. The chapter also contains extensive efficiency considerations and covers various optimizations, as well as extensions and generalizations of the notion of PCGs. Altogether, this provides a unified introduction to the work on pseudorandom correlation generators developed in my work over the past five years, aimed at a broad cryptography audience.

Jury:
Michel Abdalla, reviewer, DR CNRS at ENS Paris
Benny Applebaum, reviewer, professor at Tel-Aviv University
Ivan Damgård, examiner, professor at Aarhus University
Carmit Hazay, reviewer, professor at Bar-Ilan University
Sophie Laplante, examiner, professor at Université Paris-Cité

Proofs, programs and systems
Thursday March 21, 2024, 11AM, Salle 3052
Uli Fahrenberg Directed topology and concurrency: a personal view

Non-permanent members' seminar
Thursday March 21, 2024, 4PM, Salle 3052
Olivier Idir Explorable automata : expressiveness and decidability

Explorable automata lie on the border between deterministic and non-deterministic automata: they are non-deterministic automata where it is possible to solve the non-determinism. When given a word spelled one letter at a time, an automaton is said explorable if there exists a way to produce an accepting run by moving forward tokens in a given number of copies of the automata. (the case with exactly one copy corresponds to the history-deterministic case). In this joint work with Denis Kuperberg, I studied explorable automata on infinite words. More specifically, I studied, for different accepting conditions, their expressiveness and the decidability of the explorability property.

Higher categories, polygraphs and homotopy
Friday March 22, 2024, 2PM, Salle 3058
Sophie D'Espalungue (Université de Lille) Une théorie hiérarchique des types, ou théorie formelle des catégories (supérieures)

Automata
Friday March 22, 2024, 2PM, Salle 3052
Quentin Aristote Active Learning of Deterministic Transducers with Outputs in Arbitrary Monoids

We study monoidal transducers, transition systems arising as deterministic automata whose transitions also produce outputs in an arbitrary monoid, for instance allowing outputs to commute or to cancel out. In a first part I'll explain how Vilar's algorithm for the active learning à la Angluin of (normal) transducers generalize to monoidal transducers. In a second part I'll then discuss how this is an instance of the categorical framework for minimization and learning of Colcombet, Petrişan and Stabile: the active learning algorithm was obtained by instantiating monoidal transducers in this framework.

Verification
Monday March 25, 2024, 11AM, 3052 and Zoom link
Étienne André (LIPN) To be announced.

Formath
Monday March 25, 2024, 2PM, 3052
Lasse Blaauwbroek A machine learning platform for proof synthesis in Coq

Tactician is a proof synthesis platform that aims to make machine learning models practically accessible to Coq end-users. To this end, it makes a wide range of Coq's internal knowledge available to solving agents in a machine-learning friendly manner, including information on definitions, theorems and proofs. When the user invokes Tactician's 'synth' tactic, the solving agent is asked exploit this knowledge to complete the current proof. A wide variety of solving agents are available in the platform, including k-nearest neighbor solvers, graph neural networks, language models and random forests. Several solvers have state-of-the-art proving capabilities, far outperforming existing general purpose automation techniques. Much of this performance is due to Tactician's unique capability to learn from new knowledge on-the-fly. It can amend its models with new definitions, lemmas and proofs and immediately exploit this information during proof synthesis.

In this talk, I will give a general tutorial on Tactician. We start with a usage demonstration from an end-user perspective. Then we'll take a look at Tactician's internal architecture. There are several data formats for machine learning, including a novel graph-based representation of the Calculus of Existential Inductive Constructions, where every node in the graph represents a unique term modulo alpha-equivalence. This data is made available both as an offline dataset and through interaction with Coq using a rich remote procedure calling (RPC) protocol. We'll see how we can easily implement our own external solving agent in Python.