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

aaai_2025.jpg

10.3.2025
Congratulations to Florian Horn, co-author of Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives, a paper awarded the “Outstanding Paper Awards” at AAAI 2025.

podcast_geoffroycouteau.jpg

14.3.2025
The third episode of the CNRS podcast “Qu'est-ce que tu cherches ?” features Geoffroy Couteau, who talks about his research on data privacy protection, secure computations, and secure protocols. You will also get a glimpse into his typical day, the time when he is most productive in science (and no, it's not necessarily during the day!), and the stereotypes associated with his field. (Re)listen to this episode:

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), 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:

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:

stoc_2025.jpg

10.2.2025
Congratulations to the Adrian Vladu, IRIF member, whose paper have been accepted to STOC 2025, an ACM conference:

cnrs_editions_lecalculadecouvert.jpg

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

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

PhD defences
Friday April 4, 2025, 2PM, Amphithéâtre Gouges 1, Bâtiment Olympe de Gouges
Corentin Henriet (IRIF) Planar maps, Tamari intervals and parking trees: a bijective journey

As the title suggests, this thesis is an exploration of the bijective links between three families of combinatorial objects: planar maps, Tamari intervals and parking trees. Along the way, we will encounter many other kinds of combinatorial animals with exotic names, such as fighting fish, quadrant excursions, embedded mobiles, closed flows and blossoming trees…
Planar maps have been well known to combinatorialists since they were intro- duced about sixty years ago. Their rich underlying combinatorial structure has contributed to the development of a strong bijective framework surrounding them. We can cite the examples of bijections with blossoming trees, which allow elegant proofs of beautiful formulas counting families of planar maps. More recently, the discovery of similar formulas for Tamari intervals has led to the exploration of the bijective connection with planar maps. In this manuscript, we revisit some of these bijections and create new ones, shedding new light by integrating numerous combi- natorial families.
At the crossroads of the correspondences developed in our work, we will en- counter several models of parking trees. Not only do these trees appear naturally to encode families of planar maps and Tamari intervals, but they are also proto- types of objects governed by catalytic equations. In this sense, the general study of parking trees, initiated by Duchi and Schaeffer in 2023, and continued here, seems very promising for a further refined understanding of the bijective and enumerative schemes surrounding this manuscript.

Distributed algorithms and graphs
Tuesday April 8, 2025, 3:30PM, 3052
Laurent Viennot (IRIA et IRIF) Certificates in P and Subquadratic-Time Computation of Radius, Diameter, and all Eccentricities in Graphs

In the context of fine-grained complexity, we investigate the notion of certificate enabling faster polynomial-time algorithms. We specifically target radius (minimum eccentricity), diameter (maximum eccentricity), and all-eccentricity computations for which quadratic-time lower bounds are known under plausible conjectures. In each case, we introduce a notion of certificate as a specific set of nodes from which appropriate bounds on all eccentricities can be derived in subquadratic time when this set has sublinear size. The existence of small certificates for radius, diameter and all eccentricities is a barrier against SETH-based lower bounds for these problems. We indeed prove that for graph classes with certificates of bounded size, there exist randomized subquadratic-time algorithms for computing the radius, the diameter, and all eccentricities respectively. Moreover, these notions of certificates are tightly related to algorithms probing the graph through one-to-all distance queries and allow to explain the efficiency of practical radius and diameter algorithms from the literature.

Proofs, programs and systems
Thursday April 10, 2025, 10:30AM, Salle 3052 & online (Zoom link)
Justin Hsu (Cornell University) Type Systems for Numerical Error Analysis

Programs in numerical analysis and scientific computing make heavy use of floating-point numbers to approximate ideal real numbers. Operations on floating-point numbers incur roundoff error, and an important practical problem is to bound the overall magnitude of the error for complex computations. Existing work employs a variety of strategies such as interval arithmetic, SMT encodings, and global optimization; however, current methods are not compositional and are limited in scalability, precision, and expressivity.

Today, I'll talk about some of our recent work on NumFuzz, a higher-order language that can bound forward error using a linear, coeffect type system for sensitivity analysis combined with a novel quantitative error type. Our type inference procedure can derive precise relative error bounds for programs that are several orders of magnitude larger than previously possible.

If time permits, I'll briefly discuss a second type system called Bean for bounding backward error. Like NumFuzz, Bean is based on a linear coeffect type system, but it features a semantics based on a novel category of lenses on metric spaces. Bean is the first system to soundly reason about backward error in numerical programs.

Joint work with Ariel Kellison, Laura Zielinski, and David Bindel.

Non-permanent members' seminar
Thursday April 10, 2025, 4PM, Salle 3052
Vincent Moreau To be announced.

Automata
Friday April 11, 2025, 2PM, Salle 3052
Mahsa Shirmohammadi Differential Tree Automata

A rationally dynamically algebraic (RDA) power series is one that arises as (a component of) the solution of a system of differential equations of the form y′=F(y), where F is a vector of rational functions that is defined at y(0). RDA power series subsume algebraic power series and are a proper subclass of differentially algebraic power series (those that satisfy a univariate polynomial-differential equation). We give a combinatorial characterisation of RDA power series in terms of exponential generating functions of regular languages of labelled trees. Motivated by this connection, we define the notion of a differential tree automaton. Differential tree automata generalise weighted tree automata by allowing the transition weights to be rational functions of the tree size. Our main result is that the ordinary generating functions of the formal tree series recognised by differential tree automata are exactly the differentially algebraic power series. The proof of this result establishes a general form of recurrence satisfied by the sequence of coefficients of a differentially algebraic power series, generalising Reutenauer's matrix representation of polynomially recursive sequences. As a corollary we obtain a procedure for determining equality of differential tree automata.

The talk is based on a joint work with Rida Ait El Manssour, Vincent Cheval, and James Worrell and can be found here: https://arxiv.org/abs/2407.08218

Distributed algorithms and graphs
Tuesday April 15, 2025, 3PM, 3052
Florian Horn (IRIF) To be announced.

Proofs, programs and systems
Thursday April 17, 2025, 10:30AM, Salle 3052
Hector Suzanne (LIP6 (Sorbonne Université)) Reusable resource analysis for high-level languages

Static resource analysis is dedicated to finding methods to determine the quantity of resources (time, energy, memory, …) required to run a program, together with the variables this quantity depends on. The cornerstone of this endeavor is finding invariants/variants between program states: an analyser must automatically understand the algorithms encoded into the program without programmer input.

We focus on resource analyses through type systems for functional languages. To this aim, we introduce AutoBill, an abstract machine used as intermediate representation for resource analysis, based on the lambda-mu-mutilde calculus. We compile to this machine, amongst others, an ML-style language with data-structures (ADT), recursion (fixpoints), and some further extensions.

AutoBill uses Call-by-Push-Value operational semantics, which mixes call-by-value and call-by-name, to encode the runtime semantics of functional languages. The use of an abstract machine furthermore allows continuations to be encoded as explicit call stacks. This in turns enables the re-use of data structures analyses to analyse control flow within programs.

On top of our machine, a linear type system explicits the resource flow that accompanies jumping in and out of computations. Those types are enriched with integer parameters, that are controlled during type-checking through the addition of equations and constraints to data-type definitions. This enables the approximating sizes, costs, combinatorial invariant, etc. in a first-order constraint, and provides a link between those quantities and the largest resource usage occurring at runtime. This is done during type-inference, and the constraint is then sent to an SMT solver for validation, or to a linear programming optimizer to generate resource bounds.

We implement the “Automated Amortized Resource Analysis” method in AutoBill. It assigns, to each data-structure, a count of the amount of sub-structures with some relevant shape. This is then used to bound the iteration counts of an algorithm and obtain polynomial worst-case complexities. Our implementation consists of a specialized compilation scheme from a source language to the abstract machine. The typing-and-analysis engine is then independent of both the source language and the chosen analysis method.

Distributed algorithms and graphs
Tuesday April 22, 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).

Algorithms and complexity
Wednesday April 23, 2025, 11AM, Salle 3052
Lennart Braun (IRIF) Low-Bandwidth Mixed Arithmetic in VOLE-Based Zero-Knowledge from Low-Degree PRGs

Vector oblivious linear evaluation, or VOLE, has recently been shown to be a useful tool for designing efficient zero-knowledge proof systems that can scale to large statements with a low memory footprint (Yang et al. CCS 2021, Baum et al. CRYPTO 2021). While most ZK protocols require statements to be expressed in terms of arithmetic operations over a single finite field, recent works in VOLE-based ZK have shown how to mix Boolean and arithmetic operations in a single statement, through conversions between different finite fields (Baum et al. CCS 2021, Weng et al. USENIX 2021).

We present new, lightweight protocols for arithmetic/Boolean conversions in VOLE-based ZK. In contrast to previous works, which rely on an expensive cut-and-choose method, we take a new approach that leverages the ability of recent proof systems to prove high-degree polynomial constraints, and combines this with specialized low-degree pseudorandom generators. This not only simplifies conversions, but we showcase how it also improves the concrete efficiency of tasks important in practical ZK protocols of complex statements, including fixed point arithmetic, comparison and range proofs.

Joint work with Amit Agarwal (currently visiting IRIF), Carsten Baum, and Peter Scholl. To be presented at Eurocrypt 2025.

Verification
Monday April 28, 2025, 11AM, 3052 and Zoom link
Radu Iosif (VERIMAG, Université Grenoble Alpes) Regular Grammars for Sets of Graphs of Tree-Width 2

Regular word grammars are context-free grammars having restricted rules, that define all recognizable languages of words. This paper generalizes regular grammars from words to certain classes of graphs, by defining regular grammars for unordered unranked trees and graphs of tree-width 2 at most. The qualifier ``regular'' is justified because these grammars define precisely the recognizable (equivalently, CMSO-definable) sets of the respective graph classes. The proof of equivalence between regular and recognizable sets of graphs relies on the effective construction of a recognizer algebra of size doubly-exponential in the size of the grammar. This sets a 2EXPTIME upper bound on the (EXPTIME-hard) problem of inclusion of a context-free language in a regular language, for graphs of tree-width 2 at most. A further syntactic restriction of regular grammars suffices to capture precisely the MSO-definable sets of graphs of tree-width 2 at most, i.e., the sets defined by CMSO formulae without cardinality constraints. Moreover, we show that MSO-definability coincides with recognizability by algebras having an aperiodic parallel composition semigroup, for each class of graphs defined by a bound on the tree-width.