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 Fabian Reiter (former student at IRIF) 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. 19.2.2019 Amaury Pouly (IRIF) with François Fages, Guillaume Le Guludec and Olivier Bournez were awarded the prize "La Recherche": they have shown that chemical reactions, as the ones taking place in cells, can simulate Turing machines. Chemical reactions are universal computers. 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”. 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. 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. 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. 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. edit toutes les actualités Événements 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, 14 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 Samuele 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. Algorithmes et complexité Mardi 26 février 2019, 11 heures, Salle 1007 Uri Zwick (Tel Aviv University) Faster k-SAT algorithms using biased-PPSZ The PPSZ algorithm, due to Paturi, Pudlak, Saks and Zane, is currently the fastest known algorithm for the k-SAT problem, for every k>3. For 3-SAT, a tiny improvement over PPSZ was obtained by Hertli. We introduce a biased version of the PPSZ algorithm using which we obtain an improvement over PPSZ for every k>=3. For k=3 we also improve on Herli's result and get a much more noticeable improvement over PPSZ, though still relatively small. In particular, for Unique 3-SAT, we improve the current bound from 1.308^n to 1.307^n. Joint work with Thomas Dueholm Hansen, Haim Kaplan and Or Zamir