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 de l'IRIF Annuaire Contacts et accès Suivre @IRIF_Paris Notion du jour Actualités 9.12.2018 The Alexander von Humboldt Foundation has honored Ahmed Bouajjani (IRIF) with the prestigious Carl Friedrich von Siemens Research Award, in recognition of his research contributions. 19.11.2018 IRIF has the great pleasure to welcome Mahsa Shirmohammadi, researcher scientist (CNRS) from LIS, who is visiting IRIF for six months and who is an expert in the analysis and verification of timed, counter and probabilistic systems. 3.12.2018 Maybe you are an eager bitcoin miner? Maybe you are a fan of quantum computing too, and you wonder what will change in the mining competition when done by quantum computers? Find some answers in a paper coauthored by Miklos Santha (IRIF) to be presented at ITCS’19. 21.11.2018 Two papers coauthored by IRIF members will be presented at ITCS’19, a prestigious conference to promote research that carries a strong and innovative conceptual message in TCS. Topics include communication complexity and quantum dueling algorithms. 17.11.2018 Four papers coauthored by IRIF members will be presented at POPL’19, the main conference on programming languages and programming systems. The papers' topics are game semantics, proof theory, gradual typing, and consistency for concurrent computations. Games, gradual typing, proofs, consistency Games are mathematical objects used for modeling situations in which several participants/players interact, and each of them aims at fulfilling a personal goal. Real games such as chess or go are cases in which there are two players which are opponent. Games occur in computer science for modeling the logical duality between conjunction and disjunctions, or for defining particular families of complexity classes. Games appear in verification for describing how a system has to react to the environment (the opponent) in order to perform what it has been designed for. 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. Proof theory is the branch of mathematical logic that studies proofs as mathematical objects. In particular, proof are syntactic constructions built from axioms and inference rules. Relevant to computer science are the studies of computational and complexity aspects of proofs. Memory consistency models characterize the effect of concurrent invocations to a library implementing a shared state, e.g., a queue or a key-value map. Strong consistency means that the results of concurrently-executed invocations match the results of some serial execution of those same invocations. Since strong consistency carries a significant penalty on performance, modern implementations provide weaker guarantees known as weak consistency models, e.g., eventual or causal consistency. 20.11.2018 Two papers coauthored by IRIF members will be presented at QIP’19, the main conference for theoretical quantum information research. Topics include efficient quantum algorithms for both algebraic and distributed problems. 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. 7.10.2018 Jean-Eric Pin, CNRS senior researcher at IRIF, is awarded the Arto Salomaa prize for his outstanding contribution to the field of Automata Theory. toutes les actualités Événements Vérification lundi 10 décembre 2018, 11h10, Salle 1007 Mahsa Shirmohammadi (LIS - CNRS & Université Aix-Marseille) On the Complexity of Value Iteration Value iteration is a fundamental algorithm for solving Markov Decision Processes (MDPs). It computes the maximal n-step payoff by iterating n times a recurrence equation which is naturally associated to the MDP. At the same time, value iteration provides a policy for the MDP that is optimal on a given finite horizon n. In this talk, we settle the computational complexity of value iteration. We show that, given a horizon n in binary and an MDP, computing an optimal policy is EXP-complete, thus resolving an open problem that goes back to the seminal 1987 paper on the complexity of MDPs by Papadimitriou and Tsitsiklis. As a stepping stone, we show that it is EXP-complete to compute the n-fold iteration (with n in binary) of a function given by a straight-line program over the integers with max and + as operators. A preliminary draft of this work is available on arXiv: https://arxiv.org/abs/1807.04920v2 Graphes mardi 11 décembre 2018, 14h00, Salle 3052 Riste Škrekovski (University of Ljubljana) Some results and problems on unique-maximum colorings of plane graphs A \textit{unique-maximum} coloring of a plane graph is a proper vertex coloring by natural numbers where on each face $\alpha$ the maximal color appears exactly once on the vertices of $\alpha$. Fabrici and G\“{o}ring proved that six colors are enough for any plane graph and conjectured that four colors suffice. Thus, this conjecture is a strengthening of the Four Color Theorem. Wendland later decreased the upper bound from six to five. We first show that the conjecture holds for various subclasses of planar graphs but then we disprove it for planar graphs in general. So, we conclude that the facial unique-maximum chromatic number of the sphere is not four but five. Additionally, we will consider a facial edge-coloring analogue of the aforementioned coloring, and we will conclude the talk with various open problems. (Joint work with Vesna Andova, Bernard Lidick\'y, Borut Lu\v{z}ar, and Kacy Messerschmidt) Preuves, programmes et systèmes jeudi 13 décembre 2018, 10h30, ENS Lyon Journée Chocola () ENS Lyon http://chocola.ens-lyon.fr/events/meeting-2018-12-13/ Automates vendredi 14 décembre 2018, 14h30, Salle 3052 Colin Riba (École Normale Supérieure de Lyon) tba tba Catégories supérieures, polygraphes et homotopie vendredi 14 décembre 2018, 14h00, Salle 1007 Cameron Calk (ENS Lyon) L'homotopie dirigée et l'inversion temporelle