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.

16.11.2022
Les Assises des Mathématiques se déroulent à la Maison de l’Unesco du 14 au 16 novembre 2022. Valérie Berthé et Claire Mathieu, deux membres de l’IRIF, sont intervenues respectivement à la Table ronde sur la Synthèse nationale des Mathématiques et à la Table ronde sur les interactions entre les Mathématiques et les autres sciences.

18.11.2022
Le Hcéres a publié la synthèse nationale et de prospective sur les mathématiques. Cette synthèse est constituée de trois volumes fruit d’un travail inédit mené pendant 2 ans par le comité d’experts dont fait partie Valérie Berthé (IRIF). Volume 1 : Rapport principal. Volume 2 : Analyse disciplinaire et des interactions scientifiques. Volume 3 : Caractérisation des publications dans le monde et en France.

25.11.2022
Le prix informatique Lovelace-Babbage de l’Académie des Sciences 2023 récompense des scientifiques dont les travaux, des plus théoriques aux plus appliqués, contribuent à la création des nouvelles technologies. Date limite pour constituer son dossier de candidature : 10 décembre 2022.

23.11.2022
Nicolas Behr (IRIF) and Paul-André Melliès (IRIF) will speak at the CAP 22 conference which will take place at IHES on Monday 28 and Tuesday 29 November. The registration to the conference is free but mandatory.

18.11.2022
On November 8th, Iordanis Kerenidis (IRIF) and 5 other founding members officially launched the EQSI-European Quantum Software Institute with a stakeholder event in Paris. This initiative aims to further align development processes and jointly achieve responsible innovation in Europe for Quantum Software and Quantum Algorithms, through co-creation with industry and Quantum Hardware partners.

23.11.2022
3 papers coauthored by IRIF members will be presented at ITCS - Innovations in Theoretical Computer Science 2023.

14.11.2022
Congratulations to Olivier Carton (IRIF), head of the pole Automata, structures and verification at IRIF and recently appointed senior member of Institut universitaire de France (IUF). He is interested by the links and connexions between normality and automata.

7.11.2022
The FRAIGNIAUD workshop (Fundamental Research and Algorithmic Innovations in Graphs, Networks and the Internet, with Applications and Upcoming Directions) will take place in Paris on the 28th and 29th of November, on the occasion of Pierre FRAIGNIAUD’s 60th birthday.

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

One world numeration seminar
Mardi 29 novembre 2022, 14 heures, Online
Manuel Hauke (TU Graz) The asymptotic behaviour of Sudler products

Given an irrational number $\alpha$, we study the asymptotic behaviour of the Sudler product defined by $P_N(\alpha) = \prod_{r=1}^N 2 \lvert \sin \pi r \alpha \rvert$, which appears in many different areas of mathematics. In this talk, we explain the connection between the size of $P_N(\alpha)$ and the Ostrowski expansion of $N$ with respect to $\alpha$. We show that $\liminf_{N \to \infty} P_N(\alpha) = 0$ and $\limsup_{N \to \infty} P_N(\alpha)/N = \infty$, whenever the sequence of partial quotients in the continued fraction expansion of $\alpha$ exceeds $7$ infinitely often, and show that the value $7$ is optimal.

For Lebesgue-almost every $\alpha$, we can prove more: we show that for every non-decreasing function $\psi: (0,\infty) \to (0,\infty)$ with $\sum_{k=1}^{\infty} \frac{1}{\psi(k)} = \infty$ and $\liminf_{k \to \infty} \psi(k)/(k \log k)$ sufficiently large, the conditions $\log P_N(\alpha) \leq -\psi(\log N)$, $\log P_N(\alpha) \geq \psi(\log N)$ hold on sets of upper density $1$ respectively $1/2$.

Algorithmes et complexité
Mercredi 30 novembre 2022, 16 heures, Salle 3052
Ce Jin (MIT) Quantum Speed-ups for String Synchronizing Sets, Longest Common Substring, and k-mismatch Matching

Longest Common Substring (LCS) is an important text processing problem, which has recently been investigated in the quantum query model. The decisional version of this problem, LCS with threshold d, asks whether two length-n input strings have a common substring of length d. The two extreme cases, d = 1 and d = n, correspond respectively to Element Distinctness and Unstructured Search, two fundamental problems in quantum query complexity. However, the intermediate case 1 « d « n was not fully understood.

We show that the complexity of LCS with threshold d smoothly interpolates between the two extreme cases up to n^{o(1)} factors: LCS with threshold d has a quantum algorithm in n^{2/3 + o(1)}/d^{1/6} query complexity and time complexity, and requires at least Omega(n^{2/3}/d^{1/6}) quantum query complexity.

Our result improves upon previous upper bounds O~(min{ n/d^{1/2}, n^{2/3} }) (Le Gall and Seddighin ITCS 2022, Akmal and Jin SODA 2022), and answers an open question of Akmal and Jin.

Our main technical contribution is a quantum speed-up of the powerful String Synchronizing Set technique introduced by Kempa and Kociumaka (STOC 2019). Our quantum string synchronizing set also yields a near-optimal LCE data structure in the quantum setting, and an algorithm for the k-mismatch matching problem with k^{3/4}n^{1/2+o(1)} quantum query complexity.

Based on a SODA'23 paper joint with Jakob Nogler (ETH Zurich) and a SODA'22 paper joint with Shyan Akmal (MIT).

Algorithmes et complexité
Mercredi 30 novembre 2022, 11 heures, Salle 3052
Chris Brzuska (Aalto University) Obfuscation: Implications in Complexity and Cryptography

Obfuscation transforms a program C into a functionally equivalent program C' which hides the inner workings of C. The first formalizations of this hiding property in cryptography suffered from strong impossibility results and thus, the seemingly weak notion of indistinguishability obfuscation (iO) was formulated. It only requires that obfuscations of two circuits are indistinguishable when two circuits have equal functionality to begin with.

Although iO seems such a weak definition, it turns out surprisingly powerful (*). It allows us to transform worst-case NP problems into one-way functions, one-way functions into public-key encryption and even into fully homomorphic encryption—transformations which otherwise suffer from (black-box) separations result. In fact, iO is so strong that its existence is mutually exclusive with other assumptions which had previously been considered plausible.

At the same time, iO is also very weak; it does not even imply that P is different from NP although most cryptographic primitives (one-way functions, public-key encryption etc.) do.

In this talk, we explore the above conceptual implications. The talk is intended for a (broad) theory audience.

(*) “I must admit that I was very skeptic of the possible applicability of the notion of indistinguishable obfuscation.” Oded Goldreich when commenting on the surprising success of iO in cryptographc research.

Combinatoire énumérative et analytique
Jeudi 1 décembre 2022, 14 heures, Salle 1007 et zoom
Groupe De Lecture - Eva Philippe (Eva Philippe (IMJ-PRG)) Nu-Tamari lattice and Nu-associahedron

The goal of this talk is to present the article “Geometry of the $nu$-Tamari lattices in types A and B”, by Cesar Ceballos, Arnau Padrol, Camilo Sarmiento. We will present the nu-Tamari lattice, a generalization of the Tamari lattice where the parameter $nu$ is a lattice path. One incarnation of the nu-Catalan objects is given by the lattice paths weakly above nu. We will explain briefly how certain nu-Tamari lattices partition the usual Tamari lattice. We will focus on the geometric realization of this lattice as a triangulation of a certain polytope. This relies on another incarnation of nu-Catalan objects, the (I, J)-trees introduced by Ceballos-Padrol-Sarmiento.

Preuves, programmes et systèmes
Jeudi 1 décembre 2022, 10 heures 30, Salle 3052
David Baelde (ENS Rennes) Logical foundations of the Squirrel prover

The computationally complete symbolic attacker (CCSA) is a logically-based approach proposed by Bana and Comon to verify cryptographic protocols in the computational model, i.e. in the model of cryptographers where messages are probabilistic bitstrings and attackers are arbitrary probabilistic PTIME machines. The original formulation of CCSA was based on first-order logic and only supported the verification of protocols with bounded traces. With several co-authors, we have proposed in 2020 to build a meta-logic on top of this “base” first-order logic, to obtain a methodology that supports verifying unbounded protocols. This meta-logic forms the basis of the Squirrel proof assistant.

Soutenances de thèses
Jeudi 1 décembre 2022, 14 heures, Salle 3052 du bâtiment Sophie Germain & Zoom
Abhishek De (IRIF) Linear logic with least and greatest fixed points: truth semantics, complexity, and a parallel syntax

The subject of this thesis is the proof theory of linear logic with the least and greatest fixed points. In the literature, several systems have been studied for this language viz. the wellfounded system that relies on Park's induction rule, and systems that implicitly characterise induction such as the circular system and the non-wellfounded system. This thesis contributes to the theory of these systems with the ultimate goal of exactly capturing the provability relation of these systems and application of these objects in programming languages supporting (co)inductive reasoning. This thesis contains three parts. In the first part, we recall the literature on linear logic and the main approaches to the proof theory of logics with fixed points. In the second part, we obtain truth semantics for the wellfounded system, devise new wellfounded infinitely branching systems, and compute the complexity of provability in circular and non-wellfounded systems. In the third part, we devise non-wellfounded proof-nets and study their dynamics.

Manuscript

Automates
Vendredi 2 décembre 2022, 14 heures, Salle 3052
Léo Exibard Runtime monitoring for Hennessy-Milner logic with recursion over systems with data

Runtime verification consists in checking whether a program satisfies a given specification by observing the trace it produces during its execution. In the regular setting, Hennessy-Milner logic with recursion (recHML), a variant of the modal $\mu$-calculus, provides a versatile back-end for expressing linear- and branching-time specifications. In this talk, I will discuss an extension of this logic that allows to express properties over data values (i.e. values from an infinite domain) and examine which fragments can be verified at runtime. Data values are manipulated through equality tests in modalities and through first-order quantification outside of them. They can also be stored using parameterised recursion variables.

I then examine what kind of properties can be monitored at runtime, depending on the monitor model. A key aspect is that the logic has close links with register automata with non-deterministic reassignment, which yields a monitor synthesis algorithm, and allows to derive impossibility results. In particular, contrary to the regular case, restricting to deterministic monitors strictly reduces the set of monitorable properties.

This is joint work with the MoVeMnt team (Reykjavik University): Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Adrian Francalanza, Karoliina Lehtinen.

Vérification
Lundi 5 décembre 2022, 11 heures, 1007 and Zoom link
Kohei Suenaga (Kyoto University) HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types

(Joint work with Yuki Nishida, Hiromasa Saito, Ran Chen, Akira Kawata, Jun Furuse, and Atsushi Igarashi)

A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them. This article describes our type-based static verification tool HELMHOLTZ for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. HELMHOLTZ is designed on top of our extension of Michelson's type system with refinement types. HELMHOLTZ takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. HELMHOLTZ successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.

Algorithmes et complexité
Mardi 6 décembre 2022, 11 heures, Salle 1004
Changpeng Shao (University of Bristol) Quantum communication complexity of linear regression

In this talk, I will introduce a recent work with Ashley Montanaro. I will show you that quantum computers can have exponential speedups in terms of communication complexity for some fundamental linear algebra problems. I will mainly introduce our results on solving linear regressions. The talk is based on arXiv:2210.01601.

Sémantique
Mardi 6 décembre 2022, 10 heures 30, Salle 1007
Ariadne Si Suo (University of Oxford) Semiring Tensor and Iteration Theory

This talk is about the semantics of commutative combinations of effects.

A basic class of effects comes from the algebraic theory of modules for a semiring. The tensor of such theories is determined by the usually more tractable semiring tensor. I’ll give some examples, and then look at how the tensors work in languages with iteration. Our main contribution concerns an important class of subtheories of module theories. We observe that the subtheory tensor is also determined by the semiring tensor for several fundamental effects. I'll look at some examples of these subtheories and their tensors, and discuss how they support iteration via the underlying subsets.

This is my undergraduate summer project with Cristina Matache, Sean Moss, and Sam Staton.