Institut de Recherche en Informatique Fondamentale (IRIF)

CNRS

Université Paris Cité

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.

The EQSI is launched

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.

Accepted papers SODA 2023 - Adrian Vladu

14.11.2022
Lucas Pesenti and Adrian Vladu (IRIF) will present, at SODA 2023, their paper Discrepancy Minimization via Regularization. They make progress towards conjectures in discrepancy theory by showing that Newton's method can produce low discrepancy colorings.

Conference CAP 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.

Prix informatique Lovelace-Babbage 2023

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.

Synthèse nationale des Mathématiques

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.

Nomination IUF - Olivier Carton

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.

Assises des Mathématiques

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.

Accepted papers ITCS 2023

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


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

Vérification
Lundi 28 novembre 2022, 11 heures, 1007 and Zoom link
Nicolas Waldburger (IRISA − Université de Rennes 1) Parameterized Safety Verification of Round-Based Shared-Memory Systems

We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm [Aspnes, 2002], we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. A verification algorithm thus needs to manage both sources of infinity. In this setting, we prove that the safety verification problem, which consists in deciding whether all possible executions avoid a given error state, is PSPACE-complete. For negative instances of the safety verification problem, we also provide exponential lower and upper bounds on the minimal number of processes needed for an error execution and on the minimal round on which the error state can be covered.

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 3052 et zoom
Groupe De Lecture (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.

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 Non encore annoncé.

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

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.