Bienvenue à l'IRIF 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. Présentation Annuaire Contacts Suivre @IRIF_Paris Notion du jour Actualités (Ordonnées par priorité et aléatoire) 15.2.2019 In collaboration with Yoav Rodeh (Weizmann Institute of Science), Pierre Fraigniaud and Amos Korman from IRIF published a paper in the Journal of the ACM entitled “Parallel Bayesian Search with no Coordination”. 15.2.2019 Fabian Reiter wrote a short popularisation article in the Blog Binaire of the newspaper Le Monde. This article explains (in French) some aspects of his PhD thesis, recently awarded the Honorable Mention of the Gilles Kahn prize. 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. 23.1.2019 A CIMPA school on Graphs, Algorithms and Randomness is co-organized by Reza Naserasr from IRIF at Tabriz University, 15-22 June 2019. Three colleagues from IRIF, Pierre Fraigniaud, Michel Habib and Frédéric Magniez, are among the five lecturers from France. 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. 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. 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. 23.1.2019 FILOFOCS (French-Israeli Laboratory on Foundations of Computer Science), the first International Joint Unit in Israel, was just created by CNRS, Univ. Paris Diderot, Tel-Aviv Univ., Hebrew Univ. of Jerusalem and Weizmann Institute. IRIF hosts its “mirror site” in France, and Adi Rosén from IRIF is deputy director. edit toutes les actualités Événements Vérification Lundi 18 février 2019, 11 heures, Salle 1007 José Ignacio Requeno (Université Grenoble Alpes) Parameter Synthesis for Extended Signal Temporal Logic Specifications Cyber-Physical Systems (CPS) are complex environments composed of embedded computers that monitor or control physical processes. Nowadays, they are ubiquitously present in most aspects of our live, ranging from power stations to communications, transport or finances. Guaranteeing a correct behaviour and a good quality of service (QoS) of such critical systems is imperative. Signal temporal logic (STL) is a specification language that is adapted for dealing with continuous time real-value properties which are characteristic in CPSs. Used in combination with formal models and model checking techniques, it allows the verification and validation of runtime executions. In this talk, I will present recent improvements in the STL language; including a new method for inferring the validity domain of parametric STL specifications. Algorithmes et complexité Mardi 19 février 2019, 11 heures, Salle 3052 Danupon Nanongkai (KTH) Distributed Shortest Paths, Exactly This talk concerns the problem of quickly computing distances and shortest paths on distributed networks (the CONGEST model). There have been many developments for this problem in the last few year, resulting in tight approximation schemes. This left open whether exact algorithms can perform equally well. In this talk, we will discuss some recent progress in answering this question. Most recent works that this talk is based on are with Sebastian Krinninger (FOCS 2018) and Aaron Bernstein (ArXiv 2018). Graphes Mardi 19 février 2019, 14 heures, Salle 1007 Marthe Bonamy (CNRS - LABRI) Around Brooks' theorem In this talk, we will discuss various results around Brooks' theorem: a graph has chromatic number at most its maximum degree, unless it is a clique or an odd cycle. We will consider stronger variants and local versions, as well as the structure of the solution space of all corresponding colorings. Exposés hors-séries Mercredi 20 février 2019, 13 heures, Salle 3052 Giulio Manzonetto (LIPN) A syntactic and semantic analysis of program equivalences An important problem in theoretical computer science is to determine whether two programs are equivalent. For instance, this is needed to determine whether the optimizations performed by a compiler actually preserve the meaning of the input programs. For lambda calculi, it has become standard to consider two programs as equivalent whenever they can be plugged in any context without noticing any difference in their behavior. Such notion of equivalence depends on the behavior one is interested in observing. We provide syntactic and semantic characterizations of the equivalence arising by taking as observables the beta normal forms, corresponding to completely defined values. As a byproduct we obtain characterizations of the different degrees of extensionality in the theory of Böhm trees. Preuves, programmes et systèmes Jeudi 21 février 2019, 10 heures 30, Salle 3052 Damiano Mazza (CNRS) Intersection Types and Runtime Errors in the Pi-Calculus We introduce a type system for the $\pi$-calculus which is designed to guarantee that typable processes are well-behaved, namely they never produce a run-time error and, even if they may diverge, there is always a chance for them to “finish their work”, i.e. to reduce to an idle process. The introduced type system is based on non-idempotent intersections, and is thus very powerful as for the class of processes it can capture. Indeed, despite the fact that the underlying property is $\Pi^0_2$-complete, there is a way to show that the system is complete, i.e., that any well-behaved process is typable, although for obvious reasons infinitely many derivations need to be considered. Joint work with Ugo Dal Lago, Marc De Visme, Akira Yoshimizu Exposés hors-séries Jeudi 21 février 2019, 13 heures, Salle 3052 Pablo Arrighi (Aix-Marseille Université) Quantum, automata, computability and universality After giving a brief introduction to quantum evolutions, whether finite (automata) or infinite-dimensional (operators), I will explore their impact upon computability and universality. Most of the results I will mention rely on a decomposition of quantum operators into quantum automata, which is based upon the tacit assumption of a fixed partial order. Time-allowing, I will try to touch on the topical question of quantum partial orders. Exposés hors-séries Jeudi 21 février 2019, 11 heures 45, Salle 1007 Samule Giraudo (Université Paris-Est Marne-la-Vallée) Graded graphs and operads The set of all integer partitions admits the structure of a graded lattice, called Young lattice, which leads to a beautiful proof for the correspondence between pairs of Young tableaux of the same shape and factorial numbers. All this is due to the fact that this lattice is a differential poset, property introduced by Stanley. A generalization of this property has been provided by Fomin through graded graph duality. Some families of combinatorial objects admit such structures, and the counting of some Hasse walks reveal a nice combinatorics. We present here a new concept of graph duality, pairs of graded graphs of trees, and their lattice properties. We also show how to construct pairs of graded graphs from operads. This allows us to recover existing graphs (like the composition poset or the bracket tree) and to discover new ones. Gâteau de l'IRIF Jeudi 21 février 2019, 17 heures 30, in front of room 3052 Isaac Konan, Mahsa Shirmohammadi (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. Catégories supérieures, polygraphes et homotopie Vendredi 22 février 2019, 14 heures, Salle 1007 Cédric Ho Thanh (IRIF) The equivalence between many-to-one polygraphs and opetopic sets Automates Vendredi 22 février 2019, 14 heures 30, Salle 3052 Georg Zetzsche (MPI) Non encore annoncé. Vérification Lundi 25 février 2019, 11 heures, Salle 1007 Pierre Courtieu (CNAM) A proof framework for mobile robots protocols Distributed algorithms are known to be very difficult to design and certify. If these algorithms need to be fault or byzantine resilient the difficulty is even greater. Examples of flawed algorithms and proofs are numerous. It is therefore a natural domain for mechanized proofs (i.e. with the help of a proof assistant): the additional work of mechanizing the proofs should be worth the effort. We present a framework, named Pactole, for designing distributed protocols for mobile robots, stating properties about these protocols and proving these properties. We can also prove *impossibility statement* i.e. that there exists no protocol achieving some property. Our technique cannot be compared to but can be seen as complementary to model checking in the sense that our proofs are not automated but allow for instance to conclude that a protocol is correct *for any* starting configuration, number of robots, that is not proven impossible.