Welcome 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. Notion of the day Social Networks Follow us on Twitter/X, LinkedIn and Mastodon for our latest news: News 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 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) edit all the past news (These news are displayed using a randomized-priority ranking.) Agenda 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.