Institut de Recherche en Informatique Fondamentale (IRIF)


image/svg+xml

L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université de Paris, 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), cinq 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.

Test of Time Award – RV’21

19.10.2021
Eugene Asarin (IRIF), Alexandre Donzé, Oded Maler, and Dejan Nickovic receive the Test of Time Award at the 21st International Conference on Runtime Verification (RV’21) for their paper Parametric Identification of Temporal Properties. Watch the RV’21 Award Announcement here.

Journée de rentrée PPS 2021

7.10.2021
PPS is holding its journée de rentrée on October 13-14, 2021. This year PPS has 13 new members. The aim of this get-together is to know them and their research topic. Schedule and details of the talks here.

Accepted paper Eurocomb 2021 - Aubian-Charbit

3.9.2021
Guillaume Aubian, Pierre Charbit (IRIF) and Pierre Aboulker study the class of oriented graphs such that the out-neighbourhood of any vertex induces a transitive tournament and prove for it a decomposition theorem. As a consequence, they obtain that oriented graphs in this class have dichromatic number at most $2$ and satisfy Caccetta-Häggkvist conjecture.

Accepted paper Eurocomb 2021 - Yiting Jiang

3.9.2021
Yiting Jiang (IRIF) and Jaroslav Nešetřil will present a result that there are infinitely many minimal asymmetric k-uniform hypergraphs.

Oded Maler Best Paper Award

14.9.2021
Eugene Asarin (IRIF), Thomas Ferrère, Dejan Ničković and Dogan Ulus receive the Oded Maler best paper award in Timed Systems at the conference Formats’2021 for their paper On the complexity of timed pattern matching.

Sergio Rajsbaum - visitor at IRIF

7.9.2021
IRIF is very pleased to host for three months Sergio Rajsbaum, full time Researcher at the Instituto de Matemáticas of the Universidad Nacional Autónoma de México. This collaboration focuses on the use of algebraic topology to study the complexity of distributed algorithms. Algebraic topology tools have been mainly used for shared memory models. The purpose of the visit is to extend this research to distributed memory models. Professor Rajsbaum is partially funded by an invitational program from École Polytechnique. Meet him in office 4028a.

invited-speaker-workshop-cycles

3.9.2021
Reza Naserasr (IRIF) is an invited speaker at the 29th Workshop on Cycles and Colourings. He will present a joint work with Lan Anh Pham (IRIF), Zhouningxin Wang PhD student (IRIF) and Xuding Zhu (University Jinchua): Density of C –4 -critical signed graphs. There is a classic one-to-one correspondence between (2k+1)-colorability of a graph and mapping of a specific subdivision of it to the (2k+1)-cycle. In this work they present an extension of this to 2k-coloring using homomorphisms of signed graphs.

Accepted paper Scientific Reports

3.9.2021
Amos Korman et Robin Vacus (IRIF) publient On the Role of Hypocrisy in Escaping the Tragedy of the Commons dans la revue Scientific Reports. Dans cet article, ils étudient l'émergence de la coopération dans le cadre formel de la théorie des jeux. Ils considèrent 3 comportements stéréotypés : “tricheur”, “hypocrite” et “coopératif”, et un modèle de pression sociale.


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

Algorithmes et complexité
Mardi 19 octobre 2021, 14 heures, Salle 3052
Stephen Piddock (School of Mathematics, University of Bristol) Quantum analogue simulation: universality and complexity

Quantum analogue simulation aims to reproduce the physics of a target Hamiltonian H, using a different physical system; and this can be achieved by ensuring that the low energy subspace of the physical Hamiltonian is approximately H. First I will describe a construction of a 1D quantum system that can simulate all other Hamiltonians (a property we call universality) just by varying the length of the chain. The construction relies heavily on the possibility of encoding a (quantum) computation into the chain. Then I will go onto show a much more general equivalence between universality and the computational complexity of the Local Hamiltonian problem - the problem of approximately estimating the ground state energy of a system.

Based on https://arxiv.org/abs/2003.13753 and https://arxiv.org/abs/2101.12319

Algorithmique distribuée et graphes
Mardi 19 octobre 2021, 14 heures, Salle 1007 and via ZOOM
Mirna Džamonja (IRIF) On limits-from the finite to the countable and very much uncountable graphs

We survey several different methods of constructing infinite graphs out of the families of finite graphs, among the Fraîssé limits, the morasses, the ultraproducts and the graphons/measurings. Concentrating on a couple of them, we talk about various colourings and the generalised Ramsey theory.

Sémantique
Mardi 19 octobre 2021, 10 heures 30, Salle 3052
Théo Winterhalter (Max Planck Institute Bochum (Allemagne)) SSProve: A foundational framework for modular cryptographic proofs in Coq

State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way. While very promising, this methodology was previously not fully formalised and came with little tool support. We address this by introducing SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve combines high-level modular proofs about composed protocols, as proposed in SSP, with a probabilistic relational program logic for formalising the lower-level details, which together enable constructing fully machine-checked crypto proofs in the Coq proof assistant. Moreover, SSProve is itself formalised in Coq, including the algebraic laws of SSP, the soundness of the program logic, and the connection between these two verification styles.

One world numeration seminar
Mardi 19 octobre 2021, 14 heures 30, Online
Mélodie Lapointe (IRIF) q-analog of the Markoff injectivity conjecture

The Markoff injectivity conjecture states that $w\mapsto\mu(w)_{12}$ is injective on the set of Christoffel words where $\mu:\{\mathtt{0},\mathtt{1}\}^*\to\mathrm{SL}_2(\mathbb{Z})$ is a certain homomorphism and $M_{12}$ is the entry above the diagonal of a $2\times2$ matrix $M$. Recently, Leclere and Morier-Genoud (2021) proposed a $q$-analog $\mu_q$ of $\mu$ such that $\mu_{q\to1}(w)_{12}=\mu(w)_{12}$ is the Markoff number associated to the Christoffel word $w$. We show that there exists an order $<_{radix}$ on $\{\mathtt{0},\mathtt{1}\}^*$ such that for every balanced sequence $s \in \{\mathtt{0},\mathtt{1}\}^\mathbb{Z}$ and for all factors $u, v$ in the language of $s$ with $u <_{radix} v$, the difference $\mu_q(v)_{12} - \mu_q(u)_{12}$ is a nonzero polynomial of indeterminate $q$ with nonnegative integer coefficients. Therefore, for every $q>0$, the map $\{\mathtt{0},\mathtt{1}\}^*\to\mathbb{R}$ defined by $w\mapsto\mu_q(w)_{12}$ is increasing thus injective over the language of a balanced sequence. The proof uses an equivalence between balanced sequences satisfying some Markoff property and indistinguishable asymptotic pairs.

Combinatoire énumérative et analytique
Jeudi 21 octobre 2021, 14 heures, Salle 1007
Florent Koechlin (IRIF, Université de Paris) Séries génératrices et preuves d'intrinsèque ambiguïté

Un langage algébrique est intrinsèquement ambigu si toute grammaire qui le reconnaît est ambiguë, c'est-à-dire qu'elle génère un même mot de deux façons différentes. Décider l'intrinsèque ambiguïté d'un langage algébrique est un problème difficile, indécidable en général. Dans les années 70-80, les preuves d'intrinsèque ambiguïté reposaient essentiellement sur des raisonnements subtils et difficiles sur les arbres de dérivation des grammaires. En 1987, Philippe Flajolet a proposé une nouvelle approche pour montrer que certains langages algébriques sont intrinsèquement ambigus, en montrant que leur série génératrice n'est pas algébrique. Cette approche s'est avérée très efficace : en utilisant cette méthode, Philippe Flajolet a démontré ou redémontré dans son article l'intrinsèque ambiguïté d'une dizaine de langages, dont plusieurs étaient des conjectures de son époque. Dans cet exposé, je propose quelques extensions qui étendent le lien entre la non-ambiguïté des langages et les séries génératrices, et apportent notamment quelques pistes de réponses à deux questions posées par Philippe Flajolet à la fin de son article.

Preuves, programmes et systèmes
Jeudi 21 octobre 2021, 10 heures 15, On-line.
Armaël Guéneau (Aarhus) Program verification on a capability machine in the presence of untrusted code

Catégories supérieures, polygraphes et homotopie
Vendredi 22 octobre 2021, 14 heures, Salle 1007
Antoine Allioux (IRIF) Structures supérieures cohérentes en théorie des types homotopiques

Travail mené conjointement avec Eric Finster et Matthieu Sozeau (https://arxiv.org/abs/2105.00024).

La théorie des types de Martin-Löf peut être vue comme une fondation des mathématiques. Il a été montré que certains de ses modèles validaient une interprétation homotopique des types, ce qui a motivé une nouvelle ligne de développement de celle-ci nommée théorie des types homotopiques.

Dans cette théorie, les types ne sont pas vus comme de simples ensembles car ils ont une structure d'infini-groupoïde non-triviale conférée par leurs types identité. D'où l'idée de formaliser des résultats d'algèbre supérieure en exploitant la structure supérieure des types. Néanmoins, décrire celle-ci de façon interne reste une question ouverte. C'est à dire que l'on peut énoncer des propositions concernant des infini-groupoïdes arbitraires mais que l'on ne sait pas construire une large classe d'infini-groupoïdes, en particulier ceux dont la structure supérieure n'est pas triviale ou tronquée à partir d'une certaine dimension.

Nous proposons une approche consistant à étendre la théorie des types avec un univers de monades polynomiales satisfaisant leurs lois de façon définitionnelle. Cela nous permet de présenter les types et leur structure supérieure, et ainsi d'internaliser un certain nombre de résultats dont le fait que les types sont des infini-groupoïdes.

Automates
Vendredi 22 octobre 2021, 14 heures 30, Salle 3052
Dietmar Berwanger Telling Everything. Information Quotients in Games with Communication

Analyse et conception de systèmes
Vendredi 22 octobre 2021, 10 heures 30, Salle 1007
Théo Zimmermann (IRIF) PR of the Month: Architecture of a GitHub bot, the trigger-action model

In the context of the development of the Coq proof assistant, I have created and maintained a multi-function bot to assist developers in automating some basic and repetitive tasks. In this talk, I will present a recent pull request that was submitted to the bot repository and this will be an opportunity to present the way the bot is architectured, and how it uses a modern, typed, GitHub API and suitable OCaml libraries to implement its features, and how that makes it easy to extend.

Sémantique
Mardi 26 octobre 2021, 10 heures 30, Exposé à distance sur Galène – salle 3052 virtuelle
Thomas Ehrhard (CNRS, Université de Paris) Coherent Differentiation [Part 1]

The differential calculus uses addition in a crucial way: this appears clearly in the Leibniz Rule. This is why the differential lambda-calculus as well as differential linear logic feature an unrestricted addition operation on terms (or proofs) of the same type. From an operational point of view, this means that these formalisms feature finite non-determinism. So a natural question arises: is non-determinism inherent to any differential extension of the lambda-calculus and linear logic? Based on intuitions coming from probabilistic coherence spaces, we provide a negative answer to this question, introducing a setting of “summable categories” where the notion of summable pairs of morphisms is axiomatized by means of a functor equipped with three natural transformations satisfying a few axioms. Then we define a notion of differentiation in such a summable category equipped with a resource modality (exponential in the sense of linear logic): this differential structure is a distributive law between a monad associated with the summability structure and the resource comonad, satisfying a few additional axioms. I will present various aspects of this theory (which features similarities with tangent categories), concrete instances of the theory as well as the syntax of a differential version of PCF which can be derived from this general categorical setting. In particular I will show that coherence spaces provide a model of this coherent differentiation, in sharp contrast with differential linear logic.

One world numeration seminar
Mardi 26 octobre 2021, 14 heures 30, Online
Michael Baake (Universität Bielefeld) Spectral aspects of aperiodic dynamical systems

One way to analyse aperiodic systems employs spectral notions, either via dynamical systems theory or via harmonic analysis. In this talk, we will look at two particular aspects of this, after a quick overview of how the diffraction measure can be used for this purpose. First, we consider some concequences of inflation rules on the spectra via renormalisation, and how to use it to exclude absolutely continuous componenta. Second, we take a look at a class of dynamical systems of number-theoretic origin, how they fit into the spectral picture, and what (other) methods there are to distinguish them.