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.

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.

Fête de la Science 2021 - Conference learning about cryptography

27.9.2021
From ancient history to quantum, learn about cryptography at Fête de la science in an entertaining talk by Sylvain Perifel (IRIF). Save the date, Monday October 4th, 10am at Amphitheater 1A, Halle aux farines - Campus Grands Moulins.

Ateliers-FDSL 2021

29.9.2021
IRIF researchers are participating to the 30th edition of Fête de la Science. In different schools in Paris, they will be presenting workshops and games related to computer science.


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

Vérification
Lundi 18 octobre 2021, 11 heures, 3052 and Zoom link
Florian Renkin (LRDE, EPITA) Practical “Paritizing” of Emerson-Lei Automata

We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an ω-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a latest appearance record principle, and introduces a partial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step.

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, 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, 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 Flajolet à la fin de son article.

Preuves, programmes et systèmes
Jeudi 21 octobre 2021, 10 heures 15, On-line.
Armaël Guéneau 1) 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.

Graph Transformation Theory and Applications
Vendredi 22 octobre 2021, 15 heures, online
Frank Drewes, Berthold Hoffmann & Mark Minas (Department of Computing Science, Umeå University, Sweden; Department of Mathematics and Informatics, University of Bremen, Germany; Institute for Software Technology, Computer Science Department, Universität der Bundeswehr München , Germany) Contextual Hyperedge Replacement Grammars: Languages – Parsing – Grappa

Graph transformation allows to extend formal language theory to the generation of graph languages. This has applications in areas such as model-driven software engineering, natural language processing, and shape analysis of programs.

We start from the well-established theory of context-free grammars based on hyperedge replacement (HR) and introduces a modest extension, contextual hyperedge replacement (CHR), in order to extend their generative power. We discuss the generative power and other properties of CHR, and relate them to HR.

Then we consider parsing for CHR grammars. As for HR, parsing is NP-complete in general, so that efficient parsing algorithms can only be achieved for subclasses. We have devised two algorithms, called predictive top-down (PTD) and predictive shift-reduce (PSR), which are inspired by the well-known LL(k) and LR(k) parsing for strings, and are usually linear, at most quadratic. We illustrate the ideas of these algorithms by graph transformation rules.

Finally we demonstrate Mark Minas' graph parser generator Grappa, which implements not only PTD and PSR parsing, including the needed analysis tools, but also generalized PSR, where parallel parsing allows to cope with ambiguous grammars. Measurements of generated parsers validate our theoretical findings regarding complexity.

Zoom meeting registration link

YouTube live stream


1) Aarhus