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.

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.

Accepted paper ITCS 2023 - Sophie Laplante

30.11.2022
Sophie Laplante (IRIF) and Anupa Sunny (IRIF) will present at ITCS 2023 their paper Certificate Games in which players are given inputs x, y such that f(x)\≠f(y). Their goal is to find a position where the bits of their inputs differ. This simple new game can be used to give bounds on query complexity, block sensitivity and several other complexity measures.

Accepted papers ITCS 2023

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

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.

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 SODA 2023 - Guillaume Chapuy

14.11.2022
Guillaume Chapuy (IRIF) and Guillem Perarnau (Universitat Politècnica de Catalunya) will present, at SODA 2023, their paper proving that almost all automata with n states have a reset word not much longer than √n. This is based on a structure result saying that almost all automata are w-trees (i.e., the w-transitions induce a tree), for some very short word w — whose length is only logarithmic.

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.


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

Catégories supérieures, polygraphes et homotopie
Vendredi 2 décembre 2022, 14 heures, Attention changement de salle ! l'exposé a lieu en 4052
Nicolas Behr (IRIF) Double-categorical Compositional Rewriting Theory

Reporting on recent results of joint work with R. Harmer, P.-A. Melliès and N. Zeilberger, I will present a novel formalization of compositional rewriting theory via double categories. For a given rewriting theory, individual rewriting steps are formalized as 2-cells of a double category. One of the crucial aspects of compositionally consists then in providing a set of axioms that the double category of the rewriting system must satisfy in order to ensure the existence of concurrency and associativity theorems, which are quintessential for developing important applications of rewriting systems such as in combinatorics and Markov chain theory. Another concept central to this end, i.e., “counting modulo universal properties”, may be implemented via a certain presheaf and coend calculus. Finally, I will sketch how the counting calculus then leads to a categorification of the concept of rule algebras (which capture the combinatorics of interactions of rewriting steps).

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.

One world numeration seminar
Mardi 6 décembre 2022, 14 heures, Online
Christoph Bandt (Universität Greifswald) Automata generated topological spaces and self-affine tilings

Numeration assigns symbolic sequences as addresses to points in a space X. There are points which get multiple addresses. It is known that these identifications describe the topology of X and can often be determined by an automaton. Here we define a corresponding class of automata and discuss their properties and interesting examples. Various open questions concern the realization of such automata by iterated functions and the uniqueness of such an implementation. Self-affine tiles form a simple class of examples.

Analyse et conception de systèmes
Mercredi 7 décembre 2022, 14 heures, Salle 1007
Antoine Séré (École Polytechnique) Developments around the correction proof of Hakyber

Kyber is a key-encapsulation mechanism (KEM), whose security is based on the hardness the Module-LWE problem. It is the only KEM that has been selected by the NIST Post-Quantum Cryptography project, and will be part of NIST’s first post-quantum cryptography standard. Hakyber, a formally verified implementation of Kyber, has been developed. Hakyber is written in Jasmin, and formally verified in EasyCrypt.

EasyCrypt has already been used to prove the correction of implementations of cryptographic primitives, such as of ChaCha20-Poly1305. This proof is done by “game hopping”: the correction of a naive implementation of the primitive is proven using EasyCrypt’s probabilistic Hoare logic (pHL), and it is shown to be equivalent to gradually more optimized implementations using EasyCrypt’s probabilistic relational Hoare logic (pRHL).

Hakyber differs from the cryptographic primitives formalized in EasyCrypt by the complexity of the mathematical structures involved in it’s correctness an security proofs. In particular, it’s correction proof involves polynomials over finite fields, quotient rings and Number Theoretic Transforms (NTTs), variants of the Fourier transform used in fast polynomial multiplication algorithms.

The correction proof of Hakyber’s NTT is one of the trickiest parts of the total correction proof. We will discuss the issues we encountered in this proof, the solutions we used to overcome them, and current and planned developments of EasyCrypt that were motivated by these issues.

In particular, we will talk about the theories developed to deal with equivalence proofs of nested for loops, as well as those describing algebraic hierarchies using EasyCrypt’s clone mechanism. We will then present the planned replacement for these theories, using EasyCrypt’s annotations and type class mechanism respectively.

Combinatoire énumérative et analytique
Jeudi 8 décembre 2022, 14 heures, Salle 3052 et zoom
Amanda Burcroff (Harvard) Dyck Path Expansion Formulas for Rank 2 Cluster Algebras

The theory of cluster algebras, introduced twenty years ago by Fomin and Zelevinsky, gives us a combinatorial framework for understanding the previously opaque nature of certain algebras. Each cluster algebra is generated by its cluster variables, which are defined recursively via the process of mutation. In the rank two case, several explicit formulas have been given for the cluster variables in terms of combinatorial, representation theoretic, and tropical objects. We will focus on two such formulas. The first, given by Lee-Schiffler, sums over collections of colored Dyck subpaths, and the second, given by Lee-Li-Zelevinsky, sums over compatible pairs in Dyck paths. We will discuss a correspondence between these two sets of objects, as well as a simplification and quantum generalization of the Lee-Schiffler expansion formula.

Preuves, programmes et systèmes
Jeudi 8 décembre 2022, 10 heures 30, Salle 3052 & online ([Zoom link|https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09)
Beniamino Accattoli (INRIA Saclay, PARTOUT Project-Team) Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic.

In this talk, I will start by discussing the lack of a reasonable time cost model for linear logic. Then, inspired by recent advances in the sister field of lambda calculus, I will introduce a new term-based presentation of cut elimination for IMELL admitting a reasonable strategy (that is, a strategy of which the number of step is a reasonable time cost model). The focus will be on the principles behind the new presentation of cut elimination.

Séminaire des doctorants
Jeudi 8 décembre 2022, 16 heures, 3052 and Zoom link
Srinidhi N Domain specific language for Testing consensus implementations

I will introduce some consensus protocols and give an overview of some of the implementations. Following that, I will introduce what are the existing approaches to testing the implementations and then explain our approach which is akin to unit testing.

No prior knowledge of distributed systems/algorithms is required.