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 10.2.2025 CNRS EDITIONS has published a new book on the history of calculation, titled 𝐿𝑒 𝑐𝑎𝑙𝑐𝑢𝑙 𝑎̀ 𝑑𝑒́𝑐𝑜𝑢𝑣𝑒𝑟𝑡. Several current and former IRIF researchers contributed to the writing of this book by authoring chapters: ◻️ Part 4: ▪️ Chapter 1 - 𝑳'𝒂𝒍𝒈𝒐𝒓𝒊𝒕𝒉𝒎𝒆 : 𝒗𝒆𝒓𝒔 𝒍𝒂 𝒓𝒆́𝒔𝒐𝒍𝒖𝒕𝒊𝒐𝒏 𝒄𝒐𝒏𝒄𝒓𝒆̀𝒕𝒆 𝒅𝒆 𝒑𝒓𝒐𝒃𝒍𝒆̀𝒎𝒆𝒔 – Claire Mathieu ▪️ Chapter 2 - 𝑳𝒂 𝒄𝒐𝒎𝒑𝒍𝒆𝒙𝒊𝒕𝒆́ 𝒂𝒍𝒈𝒐𝒓𝒊𝒕𝒉𝒎𝒊𝒒𝒖𝒆 – Sylvain Perifel ◻️ Part 9: ▪️ Chapter 1 - 𝑳𝒆𝒔 𝒇𝒐𝒏𝒅𝒆𝒎𝒆𝒏𝒕𝒔 𝒅𝒖 𝒄𝒂𝒍𝒄𝒖𝒍 𝒒𝒖𝒂𝒏𝒕𝒊𝒒𝒖𝒆 – Frédéric Magniez 18.2.2025 For the CNRS conference titled « L’optimisation, au cœur des défis des sciences informatiques » (Optimization, at the core of the challenges of computer science), Simon Apers, a CNRS Research Scientist at IRIF delivered a three-minute Flash'Opti presentation about how quantum algorithm can help optimisation. The Flash'Opti presentations are a CNRS original concept designed to showcase a research topic in just three minutes, using the support of a single image. Review his speech: 17.2.2025 Science popularization for all ages! Sophie Laplante, professor at IRIF, contributed to issue 425 of Science & Vie Junior, which features an article on quantum science. After an introductory comic, it's time for clear explanations to better understand the quantum computer and demystify its promises. Encryption, keys, data, computations, and bits… These concepts are presented in an accessible way, allowing everyone, young and old, to explore the mysteries of quantum science with ease! Discover it in Science & Vie! 18.2.2025 For the CNRS conference titled « L’optimisation, au cœur des défis des sciences informatiques » (Optimization, at the core of the challenges of computer science), David Saulpic, a CNRS Research Scientist at IRIF delivered a three-minute Flash'Opti presentation about Big Data. The Flash'Opti presentations are a CNRS original concept designed to showcase a research topic in just three minutes, using the support of a single image. Take another look at his intervention: 10.2.2025 Congratulations to the Adrian Vladu, IRIF member, whose paper have been accepted to STOC 2025, an ACM conference: 22.1.2025 The third Paris ACTS, will take place at IRIF, on Wednesday 29 January. P-ACTS is a seminar series focused on connections between Automata theory and Concurrency theory, shared between EPITA, IRIF and LIX. The two speakers will be Laetitia Laversa and Glynn Winskel. The talks will also be broadcasted on Zoom. For the abstracts and more information about the seminar, see this page: 30.1.2025 Three papers of IRIF Members have been accepted to ESOP 2025. Congratulations to Giovanni Bernardi, Thomas Ehrhard, Claudia Faggian and Giulia Manara! 30.1.2025 Congratulations to Esaïe Bauer and Alexis Saurin, whose paper has been accepted for the FoSSaCS 2025 conference! edit all the past news (These news are displayed using a randomized-priority ranking.) Agenda Automata Friday March 7, 2025, 2PM, Salle 3052 Alexi Block Gorman (LIGM) A Hierarchy of Expressive Power for Büchi Automata Over the Reals There are compelling and long-established connections between automata theory and model theory, including Büchi automata and the additive group of real numbers. We say a subset X of the reals is “k-regular” if there is a Büchi automaton that accepts (one of) the base-k representations of every element of X, and rejects the base-k representations of each element in its complement. These sets often exhibit fractal-like behavior–e.g., the Cantor set is 3-regular. In this talk we will discuss the hierarchy of B\“uchi automata in terms of their expressive power–what other automata can we build from a few basic ones and (most of) the classic automata operations? We will unpack the connection between this question and first-order structures on the reals whose definable sets are all recognized by Büchi-automata. Verification Monday March 10, 2025, 11AM, 3052 and Zoom link Chiao Hsieh (Kyoto University) Certifying Lyapunov Stability of Black-Box Nonlinear Systems via Counterexample Guided Synthesis Finding Lyapunov functions to certify the stability of control systems has been an important topic for certifying safety-critical systems. Most existing methods on finding Lyapunov functions require access to the dynamics of the system. Accurately describing the complete dynamics of a control system however remains highly challenging in practice. Latest trend of using learning-enabled control systems further reduces transparency. Hence, a method for black-box systems would have much wider applications. In this talk, I will present our study on synthesizing Lyapunov functions for black-box systems. Our work stems from the idea of sampling and exploiting Lipschitz continuity to approximate the unknown dynamics. Given Lipschitz constants, one can derive a *non-statistical upper bounds* on approximation errors; hence a strong certification on this approximation can certify the unknown dynamics. We significantly improve this idea by directly approximating the Lie derivative of Lyapunov functions instead of the dynamics. We propose a framework based on the learner–verifier architecture from Counterexample-Guided Inductive Synthesis (CEGIS). Our insight of combining regional verification conditions and counterexample-guided sampling enables a guided search for samples to prove stability region-by-region. Our CEGIS algorithm further ensures termination. Our numerical experiments suggest that it is possible to prove the stability of 2D and 3D systems with a few thousands of samples. In comparison with the existing black-box approach using evenly-spaced sampling, our approach at the best case requires less than 0.01% of samples. The paper describing our latest results will be published in May at the conference on Hybrid Systems: Computation and Control 2025. Enumerative and analytic combinatorics Tuesday March 11, 2025, 11AM, Salle 3071 Hadrien Notarantonio To be announced. Distributed algorithms and graphs Tuesday March 11, 2025, 2PM, 3052 Pascal Préa (École Centrale Méditerranée) A simple & optimal algorithm for strict circular seriation The goal of circular seriation is, given a set X and a dissimilarity d on X (we can see d as a complete valued graph on X, or as a distance (without the triangular inequality)), to determinate if X can be represented on a circle in a a way which is ‘’compatible’’ with d. There exist 4 non-equivalent definitions of this problem. We will present these four definitions and a simple and optimal algorithm for the two most interesting ones, at least in the ‘’strict’’ case (the inequalities that defines the problems are strict). Semantics Wednesday March 12, 2025, 10:45AM, Salle 3071 Elena Di Lavore (Oxford) Effectful streams for dataflow programming Effectful streams give formal compositional coinductive semantics to effectful synchronous dataflow programs. Effectful streams allow us to develop notions of trace and bisimulation for effectful Mealy machines; bisimilarity implies effectful trace equivalence. This talk is based on joint work with Giovanni de Felice and Mario Román, and on more recent joint work with Filippo Bonchi and Mario Román. Proofs, programs and systems Thursday March 13, 2025, 10:30AM, Amphithéâtre Alan Turing Maribel Fernandez, Victoria Barrett, Elena Di Lavore CHOCOLA seminar series https://chocola.ens-lyon.fr/events/meeting-2025-03-13/ Non-permanent members' seminar Thursday March 13, 2025, 4PM, Salle 3052 Benjamin Mathieu-Bloise To be announced. Distributed algorithms and graphs Tuesday March 18, 2025, 3PM, 3052 Fabien De Montgolfier (IRIF) Beating LexBFS with BFS and DFS In this talk I will present a work in progress : how simple graph searches such as Depth First Search (DFS) or Breadth First Search (BFS) can be used to recognize simple structured classes of graphs. For these three classes, Trivially Perfect graphs, Proper Interval graphs (aka Unit Interval Graphs), and Chordal graphs, the simplest (among linear-time) known algorithms use LexBFS instead (applied once or thrice). Semantics Tuesday March 18, 2025, 3PM, Salle 3071 Vladimir Zamdzhiev (LORIA) To be announced. PhD defences Tuesday March 18, 2025, 4:30PM, Amphithéâtre Turing, Bâtiment Sophie Germain Dung Bui (IRIF) Efficient Secure Computation from Correlated Pseudorandomness In this thesis, we put forward advancements in Multi-Party Computation (MPC), enabling parties to jointly compute arbitrary functions while preserving the privacy of their inputs. Our focus is on MPC with correlated randomness, where efficiency is improved through correlations generated using preprocessing. We investigate two key paradigms for generating such randomness: Pseudorandom Correlation Generators (PCGs) and Pseudorandom Correlation Functions (PCFs). First, we propose new PCG-based constructions for Private Set Intersection (PSI), achieving either tighter security or improved performance. We then explore the applications of PCGs and PCFs in Zero-Knowledge Proofs (ZKPs), addressing both interactive and non-interactive settings. For interactive ZKPs, we design a privately verifiable protocol for circuit satisfiability with sublinear communication and efficient computation. In the non-interactive setting, we introduce a new designated-verifier ZKP (DV-NIZK) leveraging PCF with a public-key structure (PK-PCF). Finally, we introduce a novel MPC framework for binary circuits, utilizing a PCG optimized for small fields.