Welcome to IRIF IRIF, the Research Institute on the Foundations of Computer Science, is a research laboratory of CNRS and Université Paris-Diderot, also hosting two INRIA project-teams. The research conducted at IRIF is based on the study and understanding of the foundations of all computer science, in order to provide innovative solutions to the current and future challenges of digital sciences. IRIF hosts about 200 people. Six of its members have been distinguished by the European Research Council (ERC), three are members of the Institut Universitaire de France (IUF), and two are members of the Academia Europæa. Presentation of IRIF Members Contact and access Follow @IRIF_Paris Notion of the day News (randomized-priority ranking) 16.1.2019 Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani from IRIF present this week at POPL19 a paper coauthored with Jeremy Siek (Indiana university) about a new formal framework for gradual typing allowing a smoother and more declarative integration of gradual typing in existing programming languages. 17.1.2019 Guillaume Chapuy and Enrica Duchi from IRIF coorganize with Christina Goldschmidt (Oxford) the Journées Aléa 2019, a CNRS thematic school about discrete random structures, from 03-18 to 03-22 at CIRM. Register by January 23. 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. 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. 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. 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. edit all the news Events Complex systems Tuesday January 22, 2019, 2PM, Salle 3052 Guillaume Ducoffe (ICI Roumanie) Computing Giant Diameters with Breadth-First Search and Range Queries A well-known problem for which it is difficult to improve the textbook algorithm is computing the graph diameter. We present two versions of a simple algorithm (one being Monte Carlo and the other deterministic) that for every fixed $h$ and unweighted undirected graph $G$ with $n$ vertices and $m$ edges, either correctly concludes that $diam(G) < hn$ or outputs $diam(G)$, in time ${\cal O}(m+n^{1+o(1)})$. The algorithm combines a simple randomized strategy for this problem (Damaschke, {\it IWOCA'16}) with a popular framework for computing graph distances that is based on range trees (Cabello and Knauer, {\it Computational Geometry'09}). We also prove that under the Strong Exponential Time Hypothesis (SETH), we cannot compute the diameter of a given $n$-vertex graph in truly subquadratic time, even if the diameter is an $\Theta(n/\log{n})$. Graphs Tuesday January 22, 2019, 2PM, Salle 3052 Guillaume Ducoffe (ICI Roumanie) Computing Giant Diameters with Breadth-First Search and Range Queries A well-known problem for which it is difficult to improve the textbook algorithm is computing the graph diameter. We present two versions of a simple algorithm (one being Monte Carlo and the other deterministic) that for every fixed $h$ and unweighted undirected graph $G$ with $n$ vertices and $m$ edges, either correctly concludes that $diam(G) < hn$ or outputs $diam(G)$, in time ${\cal O}(m+n^{1+o(1)})$. The algorithm combines a simple randomized strategy for this problem (Damaschke, {\it IWOCA'16}) with a popular framework for computing graph distances that is based on range trees (Cabello and Knauer, {\it Computational Geometry'09}). We also prove that under the Strong Exponential Time Hypothesis (SETH), we cannot compute the diameter of a given $n$-vertex graph in truly subquadratic time, even if the diameter is an $\Theta(n/\log{n})$. Proofs, programs and systems Thursday January 24, 2019, 10:30AM, Ens Lyon Seminaire Chocola (Ens Lyon) To be announced. IRIF Cake Thursday January 24, 2019, 5:30PM, in front of room 3052 Antoine Allioux, Thomas Colcombet, Chaitanya Leena-Subramaniam, Amaury Pouly (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. Automata Friday January 25, 2019, 2:30PM, Salle 3052 Nathan Grosshans To be announced. Verification Monday January 28, 2019, 11AM, Salle 1007 Mark Batty (University of Kent) A denotational semantics for weak-memory language concurrency with modular DRF-SC Concurrent languages provide weak semantics: they admit non-sequentially-consistent (SC) behaviour to accommodate weak target architectures and compiler optimisation. Subtle behaviour and intricate specifications result, but two properties help to simplify things – no thin-air values, and DRF-SC. In the first, all values must be computed from constants or inputs to the program, rather than conjured up, for example, through abuse of speculative execution. In DRF-SC, programs without data races are guaranteed SC behaviour. Unfortunately, existing languages like C/C++ admit thin-air values and DRF-SC results only apply to an unrealistic class of programs, excluding systems code and code using concurrency libraries. We provide a modular semantics that avoids thin-air values and we prove a new modular variant of DRF-SC that lifts a key barrier to its usefulness. Semantics Monday January 28, 2019, 11AM, Salle 3052 Fredrik Dahlqvist (UCL - Department of Computer Science) Semantics of higher-order probabilistic programs with conditioning We present a denotational semantics for higher-order probabilistic programs in terms of linear operators between Banach spaces. Our semantics is rooted in the classical theory of Banach spaces and their tensor products, but bears similarities with the well-known semantics of higher-order programs à la Scott through the use ordered Banach spaces which allow definitions in terms of fixed points. Being based on a monoidal rather than cartesian closed structure, our semantics effectively treats randomness as a resource. Algorithms and complexity Tuesday January 29, 2019, 11AM, Salle 1007 Balthazar Bauer (ENS) An application of communication complexity to cryptography The hash function are very important primitives in cryptology. To use it, we need to trust the designer. To solve this problem, we can combine several hash functions independently built. But we have to suppose that the designers could communicate. That's why we can reduce the security properties to communication complexity problems. After a presentation of these reductions, we will look in details the communication problems linked to these properties, our knowledge, new results about them. And at the end the open problems that challenge us will be presented. Semantics Tuesday January 29, 2019, 11AM, Salle 3052 Giulio Guerrieri (Università di Bologna) Non-idempotent intersection types for call-by-need lambda calculus