L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris-Diderot, qui héberge deux équipes-projets 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), trois sont membres de l'Institut Universitaire de France (IUF) et deux sont membres de l'Academia Europæa.

(Ordonnées par priorité et aléatoire)

Uri Zwick

15.3.2019
From March 20th to May 22nd, Uri Zwick (Univ. of Tel Aviv) will give a series of 7 courses related to his FSMP Chaire of Excellence on the topic of Games on Graphs and Linear Programming Abstractions each Wednesday 2:15pm - 4:15pm at IRIF, room 3052.

14.3.2019
FSMP offers 21 PhD student positions in Maths and TCS under H2020 COFUND project MathInParis. As a member of the FSMP network, IRIF is an eligible hosting lab. Call for application is open until April, 1st 2019. Applicants must be international students, but master students already in France for less than a year are eligible.

Uri Zwick

1.2.2019
IRIF has the great pleasure to welcome Uri Zwick, professor at the Blavantik School of Computer Sience (University of Tel-Aviv), who is visiting for four months. His stay is financed by an FSMP chair. Uri is an expert in algorithms, data structures and games. Meet him in office 4048.

Ile de France

17.3.2019
The Paris Region PhD2 program will grant 30 PhD projects on Digital Sciences and with an industrial partner. IRIF is an eligible hosting lab. Call for application is open until May, 15th 2019.

logo-cirm.jpg

5.11.2018
Amélie Gheerbrand and Cristina Sirangelo from IRIF co-organize with L. Libkin, L. Segoufin, and P. Senellart, the 2019 Spring School on Theoretical Computer Science (EPIT) on Databases, Logic and Automata, to happen the 7-12 April 2019 in Marseille. Preregistration before 13 January 2019.

17.1.2019
Pierre Fraigniaud from IRIF organizes the Workshop Complexity and Algorithms (CoA), in the framework of GdR IM, Roscoff, France, April 1-5, 2019. The objective of this workshop is to gather the French community on design and analysis of algorithms, of all forms. Deadlines: submission by 01/02/2019, registration by 02/03/2019.

Amaury Pouly

8.1.2019
IRIF has the great pleasure to welcome a new researcher (CNRS), Amaury Pouly, an expert in continuous models of computations, and the analysis and verification of continuous/hybrid dynamical systems.

Jeremy Siek

9.1.2019
IRIF has the great pleasure to welcome Jeremy Siek, professor at Indiana University Bloomingtom, who is visiting IRIF for five months. Jeremy is the creator of gradual typing and a world-renowed expert in typed programming languages. Meet him in office 4034a.
gradual typing

Gradual typing is a technique that allows the programmer to control which parts of a program check their type correctness (i.e., that apples are added to apples) before execution and which parts check it during their execution instead. It is often used to gradually add the before-execution check to dynamic languages, like JavaScript, which perform the check only at run-time, since it is generally better to find errors before the execution of a program rather than during its execution.

Preuves, programmes et systèmes
Jeudi 21 mars 2019, 10 heures 30, Salle 3052
Paolo Pistone (Univ. Tubingen) Quelques résultats sur l'équivalence des preuves dans la logique linéaire du second ordre

Les réseaux de preuves donnent une représentation canonique des démonstrations dans la logique linéaire multiplicative : l'équivalence dénotationnelle des preuves coïncide avec l'équivalence des réseaux. Par contre, la canonicité des réseaux ne s'étend pas au second ordre. Ce problème est du à la présence des témoins des règles existentielles. En fait, dans plusieurs sémantiques dénotationnelles l'information portée par les preuves est compressée, et notamment les témoins existentiels sont effacés.

Font partie de ces sémantiques “effaçantes” les sémantiques cohérente et rélationnelle, ainsi que la sémantique dinaturelle et la sémantique observationnelle. On présente des résultats sur l'équivalence des preuves dans ces sémantiques et on discute des applications en complexité dues à la possibilité de compresser les preuves. Une partie de ces travaux est issue d'une collaboration avec L. Tortora de Falco, T. Seiller et L.T.D. Nguyễn.

Exposés hors-séries
Jeudi 21 mars 2019, 13 heures, Salle 3052
Reem Yassawi (Université de Lyon) Les automates cellulaires et dynamique symbolique

Les automates cellulaires sont des objets qui peuvent être interprétés, d’un point de vue informatique, comme modèles de calculs parallèles, ou d’un point de vue mathématique, comme systèmes dynamiques. Ils forment donc un pont entre deux domaines de science apparement éloignés. Je donne un bref survol de la théorie des automates cellulaires en dynamique symbolique. Ensuite j’expose deux problèmes différents autour des automates cellulaires auxquels je me suis intéressée.

Le premier problème concerne les propriétés de randomisation de certains automates cellulaires. La randomisation asymptotique est le processus par lequel un état initial de basse entropie est asymptotiquement transformée en un état d'entropie maximale, par l’action itérée de l’automate cellulaire. Je discute des conditions nécessaires et suffisantes pour qu’une telle randomisation survienne, et aussi d'un travail récent avec Eric Rowland.

La deuxième problématique est de caractériser les automates cellulaires qui préservent un langage donné. Je résume un travail récent avec Clemens Muellner, où nous obtenons un théorème de structure pour les automates cellulaires qui préservent certains langages HD0L.

Gâteau de l'IRIF
Jeudi 21 mars 2019, 17 heures 30, in front of room 3052
Simon Maurras (IRIF CakeTM) Gâteau de l'IRIF

IRIF CakeTM is an amazing opportunity to meet people while simultaneously eating cakes baked by your fellow colleagues! Join us every Thursday, at 5pm, in front of room 3052 (Sophie Germain 3rd floor) for a weekly feast. You can also express your cooking skills and volunteer to bake a cake by sending an email to cake@irif.fr.

Automates
Vendredi 22 mars 2019, 14 heures 30, Salle 3052
Reem Yassawi (CNRS, Institut Camille Jordan - Université Lyon 1 - Claude Bernard) Versions quantitatives du théorème de Christol

Pour une suite $\mathbb{a} = (a_n)_{n≥0}$ à valeurs dans un corps fini $\mathbb{F}_q$, le théorème de Christol établit une équivalence entre $q$-automaticité de $\mathbb{a}$ ($\mathbb{a}$ calculable par un automate) et l’algebricité de la série formelle $f(x) = \sum a_n x^n$. Dans ce travail nous étudierons le nombre d’états de l’automate en fonction des paramètres du polynôme annulateur minimal de $f(x)$.

Andrew Bridy a récemment donne une démonstration du théorème de Christol en utilisant des outils qui proviennent de la géométrie algébrique. Avec cette démonstration il majore le nombre d’états par une borne qui est optimale. Nous obtenons des bornes presque semblables par une démonstration élémentaire, et nous traçons les liens entre notre démonstration et celle de Bridy. Ceci est un travail en commun avec Boris Adamczewski.

Vérification
Vendredi 22 mars 2019, 11 heures, 3052
Matteo Maffei (TU Wien) Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts

The recent growth of the blockchain technology market puts its main cryptocurrencies in the spotlight. Among them, Ethereum stands out due to its virtual machine (EVM) supporting smart contracts, i.e., distributed programs that control the flow of the digital currency Ether. Being written in a Turing complete language, Ethereum smart contracts allow for expressing a broad spectrum of financial applications. The price for this expressiveness, however, is a significant semantic complexity, which increases the risk of programming errors. Recent attacks exploiting bugs in smart contract implementations call for the design of formal verification techniques for smart contracts. This, however, requires rigorous semantic foundations, a formal characterization of the expected security properties, and dedicated abstraction techniques tailored to the specific EVM semantics.

This talk will overview the state-of-the-art in smart contract verification, covering formal semantics, security definitions, and verification tools. We will then focus on EtherTrust, a framework for the static analysis of Ethereum smart contracts that we recently designed, which includes the first complete small-step semantics of EVM bytecode, the first formal characterization of a large class of security properties for smart contracts, and the first steps towards a static analysis for EVM bytecode, based on Horn clause resolution, that comes with a proof of soundness.

Graphes
Vendredi 22 mars 2019, 14 heures, Salle 1007
Julien Baste (Universität Ulm, Ulm, Germany) Hitting minors on bounded treewidth graphs

For a fixed collection of graphs F, the F-DELETION problem consists in, given a graph G and an integer k, decide whether there exists S, subset of V(G), with |S| ⇐ k such that G-S does not contain any of the graphs in F as a minor. This NP-hard problem is a generalization of some well known graph problems as VERTEX COVER (F={K_2}), FEEDBACK VERTEX SET (F={K_3}), or VERTEX PLANARIZATION (F={K_5,K_{3,3}}). We are interested in its parameterized complexity when the parameter is the treewidth of G, denoted by tw. Namely, the objective is to determine, for a fixed F, the (asymptotically) smallest function f_F: N → N such that F-DELETION can be solved in time f_F(tw)*n^{O(1)} on n-vertex graphs. In this talk we will provide the basic definitions of parameterized complexity, motivate the problem, and then, review some of the lower and upper bounds on the function f_F for several instantiations of F.

The presented results are joint work with Ignasi Sau and Dimitrios Thilikos and can be found in <https://arxiv.org/abs/1704.07284>.

Vérification
Lundi 25 mars 2019, 11 heures, Salle 1007
Cristoph Kirsch (Universität Salzburg) On the Self in Selfie

Selfie is a self-contained 64-bit, 10-KLOC implementation of (1) a self-compiling compiler written in a tiny subset of C called C* targeting a tiny subset of 64-bit RISC-V called RISC-U, (2) a self-executing RISC-U emulator, (3) a self-hosting hypervisor that virtualizes the emulated RISC-U machine, and (4) a prototypical symbolic execution engine that executes RISC-U symbolically. Selfie can compile, execute, and virtualize itself any number of times in a single invocation of the system given adequate resources. There is also a simple linker, disassembler, debugger, and profiler. C* supports only two data types, uint64_t and uint64_t*, and RISC-U features just 14 instructions, in particular for unsigned arithmetic only, which significantly simplifies reasoning about correctness. Selfie has originally been developed just for educational purposes but has by now become a research platform as well. We discuss how selfie leverages the synergy of integrating compiler, target machine, and hypervisor in one self-referential package while orthogonalizing bootstrapping, virtual and heap memory management, emulated and virtualized concurrency, and even replay debugging and symbolic execution.

This is joint work with Alireza S. Abyaneh, Simon Bauer, Philipp Mayer, Christian Mösl, Clément Poncelet, Sara Seidl, Ana Sokolova, and Manuel Widmoser, University of Salzburg, Austria.

Web: http://selfie.cs.uni-salzburg.at

Algorithmes et complexité
Mardi 26 mars 2019, 11 heures, Salle 1007
Alexander Knop (UC San Diego) On proof systems based on branching programs

It is well known that there is a connection between resolution complexity of a formula and complexity of (very weak) branching programs for the corresponding search problem. In the talk, we will discuss proof systems that allow to generalize this statement and explain the lower bounds for these proof systems. In order to achieve this lower bounds, we show how to transform functions with a high fixed-partition communication complexity into functions with a high best-partition communication complexity and as a result, we translate the landscape of fixed-partition communication complexity classes into the landscape of best-partition communication complexity classes.

Systèmes complexes
Mardi 26 mars 2019, 14 heures, Salle 3052
Anaïs Durand (LIP6, Sorbonne Université) Contention-related crash failures

In the literature, two kinds of process crashes are usually considered: initially dead processes and “classical” crash failures (that can occur at any time). A new notion of process failure explicitly related to contention has recently been introduced by Gadi Taubenfeld (NETYS 2018). More precisely, given a predefined contention threshold λ, this notion considers the execution in which process crashes are restricted to occur only when process contention is smaller than or equal to λ. If crashes occur after contention bypassed λ, there are no correctness guarantees. It was shown that, when λ = n-1, consensus can be solved in an n-process asynchronous read/write system despite the crash of one process, thereby circumventing the well-known FLP impossibility result.

In this talk, I will present k-set agreement and renaming algorithms that are resilient to two types of process crash failures: “λ-constrained” crash failures (as previously defined) and classical crash failures.

Exposés hors-séries
Mardi 26 mars 2019, 16 heures, Salle 3052
Marc Pouzet (ENS Paris) Zelus, un langage synchrone fonctionnel pour les systèmes hybrides

Le parallélisme synchrone est utilisé aujourd'hui de manière routinière pour concevoir et implémenter le logiciel de controle/commande critique, dans les avions ou les train, par exemple. Il permet d'écrire un modèle mathématique idéal du système en faisant l'hypothèse que tous les processus partagent une échelle de temps globale commune. On raisonne d'abord en négligeant les temps de calculs et de communication, ce qui simplifie la détection de certaines erreurs (interblocages, courses critiques) et les étapes de validation (simulation, test, vérification formelle). Puis on vérifie que le code généré par le compilateur respecte les contraintes de temps d'exécution pire-cas.

Les langages synchrones décrivent des systèmes à temps discret seulement. Ils ne permettent pas de modéliser, ni fidèlement ni très efficacement des systèmes contenant des dynamiques hybrides combinant des signaux à temps discret et à temps continu. Cela créé une rupture dans la chaîne de développement, avec un langage pour la modélisation hybride et un autre pour la modélisation ou l'implémementation du logiciel de contrôle.

Dans cet exposé, nous présenterons Zelus, une extension d'un langage synchrone avec des équations différentielles ordinaires (ODEs) et une opération de détection d'événement (zero-crossing). Il permet d'écrire dans un source unique, un modèle synchrone (à temps discret) du logiciel de controle et un modèle (à temps discret où à temps continu) de son environnement. Nous illustrerons le langage sur quelques exemples. Nous présenterons son système de types qui permet de cloisonner les parties à temps discret et les parties à temps continu pour rejeter des comportements étranges que l'on obtient avec les outils de modélisation hybrides les plus utilisés. Nous montrerons également son analyse par typage des boucles de causalité par typage. Enfin, nous montrerons le principe utilisé pour générer du code séquentiel qui est lié ensuite à un solveur numérique (ici Sundials Cvode). Si le temps le permet, nous discuterons une expérimentation en cours, d'ajout de contructions de programmes probabilistes, ainsi que quelques questions ouvertes autour du typage, de la sémantique et de la vérification.

Logique, automates, algèbre et jeux
Mercredi 27 mars 2019, 14 heures 15, 3052
Uri Zwick (Blavatnik School of Computer Science) Games on Graphs and Linear Programming Abstractions, Part 2/7: Mean Payoff games and Energy Games

In this talk we consider non-stochastic versions of the games introduced in the first lecture, namely Mean Payoff Games (MPGs) and Energy Games (EGs). We show reductions between these two games. We then describe a pseudo-polynomial time algorithm of Brim et al. for EGs, and hence also MPGs

https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf

Preuves, programmes et systèmes
Jeudi 28 mars 2019, 10 heures 30, Salle 3052
Thomas Leventis (Univ. Bologna (Italy)) Taylor expansion of probabilistic lambda-terms

Taylor expansions have been introduced by Ehrhard and Regnier as a computational interpretation of Girard's quantitative semantics. Lambda-terms are expanded into linear combinations of their n-linear approximants, such approximants being defined as resource lambda-terms. This construction is well-suited to interpret quantitative calculi, such as the probabilistic lambda-calculus: Taylor expansions are linear combinations and the resource lambda-calculus is linear so interpreting probability distributions over terms is straightforward. Yet paradoxically the proof technique used by Ehrhard and Regnier to study Taylor expansions heavily rely on the particular structure of the expansions of ordinary lambda terms, and they are not suited to work on a quantitative setting. In this talk we will show how to indirectly extend their result to probabilistic Taylor expansions. First we will introduce explicit Taylor expansions, which uses “inert” probabilistic choices to interpret probabilistic terms while preserving the necessary properties to apply Ehrhard and Regnier's proof techniques. Then we will show how to extract interesting results on probabilistic Taylor expansions from these explicit Taylor expansions.