## Welcome to IRIF

IRIF, the Research Institute on the Foundations of Computer Science, is a research laboratory of CNRS and Université de Paris, 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), five are members of the Institut Universitaire de France IUF), and two are members of the Academia Europæa.

## Notion of the day

## News

*11.12.2019*

**Two papers** coauthored by IRIF members will be presented at POPL’20, the main conference on programming languages and programming systems. The papers' topics are reflecting Coq in Coq and how to differentiate higher-order programs.

*10.12.2019*

Michele Pagani (IRIF), Alois Brunel (Deepomatic) and Damiano Mazza (LIPN) will present at POPL'20 an effect-free extension of the backpropagation algorithm to higher-order functional programming, allowing for a logical understanding of its dynamics thanks to linear logic.

*13.12.2019*

Raphaëlle Crubillé (former student at IRIF) was awarded the Gilles Khan 2019 prize for her PhD thesis entitled « Behavioral Distances for Probabilistic Higher-order Programs » supervised by Thomas Ehrhard at IRIF.

*8.10.2019*

The SODA 2020 conference will include a paper by Vincent Cohen-Addad (LIP6), Frederick Mallmann-Trenn (King's College) and Claire Mathieu (IRIF) about computing with noisy data. The problem: select valuable objects in a setting where each assessment has a probability of error, using redundant assessments.

*16.10.2019*

On **December 16th**, a half-day of talks aimed at a non-specialized audience will take place at IRIF in celebration of **Algorithms**, the research domain of Claire Mathieu, 2019 recipient of a **CNRS Silver Medal**. The event will conclude with a discussion of new research directions in Algorithms. Free Registration before November 30th.

(These news are displayed using a randomized-priority ranking.)

## Events

Algorithms and complexity

Monday December 16, 2019, 12:30AM, Amphi Turing

**M. Teillaud, T. Starikovskaya, M. Bonamy, C. Mathieu** *Autour des algorithmes*

Programme :

12h30-13h15 : Accueil et café

13h15-13h30 : Ouverture

13h30-14h15 : Exposé de Monique Teillaud, Autour des triangulations de Delaunay

14h15-15h : Exposé de Tatiana Starikovskaya, Streaming algorithms for string processing

15h-15h45 : Exposé de Marthe Bonamy, Complexity of graph coloring

15h45-16h15 : goûter

16h15-17h : Exposé de Claire Mathieu, Rank Aggregation

17h-18h : Table ronde “Prospectives de l'algorithmique en France” animée par Claire Mathieu. Participantes : Anne Boyer, Ioana Manolescu et Camille Terrier.

Verification

Monday December 16, 2019, 11AM, Salle 1007

**Jules Villard** (Facebook) *The Infer Static Analysis platform*

This talk will present how Infer is used at Facebook, where it analyses thousands of code changes every month, leading to thousands of bugs being found and fixed before they reach users. We will then see how to write your own inter-procedural static analysis in just a few lines of code inside Infer, and automatically be able to apply it to millions of lines of code.

PhD defences

Monday December 16, 2019, 2:30PM, Salle 2017, Bâtiment Sophie Germain

**Adrien Husson** (IRIF) *Logical foundations of a modelling assistant for molecular biology*

Manuscript

Automata

Tuesday December 17, 2019, 2:30PM, Salle 0010

**Achim Blumensath** (Masaryk University) *Regular Tree Algebras*

Noter la salle et l'horaire inhabituels.

Algorithms and complexity

Tuesday December 17, 2019, 11AM, Salle 1007

**Clément Canonne** (IBM Research) *Uniformity Testing for High-Dimensional Distributions: Subcube Conditioning, Random Restrictions, and Mean Testing*

This is the “subcube conditional sampling model”, first considered in Bhattacharyya and Chakraborty (2018). We provide a nearly optimal ~O(sqrt{d})-algorithm for testing uniformity in this model. The key component of our proof is a natural notion of random restriction for distributions on {-1,1}^d, and a quantitative analysis of how such a restriction affects the mean vector of the distribution. Along the way, we provide a /very/ nearly tight upper bound on the (standard) sample complexity of a natural problem, “mean testing.”

Joint work with Xi Chen, Gautam Kamath, Amit Levi, and Erik Waingarten.

Semantics

Tuesday December 17, 2019, 10:30AM, Salle 3052

**Yannick Zakowski** (Irisa/Inria) *From representing recursive and impure programs in Coq to a modular formal semantics of LLVM IR*

In this talk, we will focus on the design and implementation of Interaction Trees (ITrees), a general-purpose data-structure for representing in Coq potentially divergent, effectful, programs. ITrees are built out of uninterpreted events and their continuations. They support compositional construction of interpreters from event handlers, which give meaning to events by defining their semantics as monadic actions. They are expressive enough to represent impure and potentially nonterminating, mutually recursive computations in Coq. Finally, they give rise to a theory enabling equational reasoning, up to weak bisimulation, about ITrees and monadic computations built from them. In contrast to other approaches, ITrees are executable via code extraction.

ITrees are expressive enough to serve as a language of specification for most projects of the DeepSpec ecosystem, making them a sort of Franca Lingua for formal specification, and helping in connecting projects together. Furthermore, their ability to be extracted make them compatible with ambitions of liveness and two-sidedness.

In a second part of this talk, we will focus on how ITrees are used in one of the DeepSpec projects in particular: Vellvm. More specifically, we will give an account of the ongoing effort to use ITrees as a mean to define a modular formal semantics of LLVM IR.

PhD defences

Tuesday December 17, 2019, 10AM, 0010

**Mengchuan Zou** *Aspects of Efficiency in Selected Problems of Computation on Large Graphs*

PhD defences

Tuesday December 17, 2019, 10AM, Salle 0010, Bâtiment Sophie Germain

**Mengchuan Zou** (IRIF) *Aspects of Efficiency in Selected Problems of Computation on Large Graphs*

In the first work, we consider a setting of classical centralized computing, and we consider the question of generalizing modular decompositions and designing time-efficient algorithm for this problem. Modular decomposition, and more broadly module detection, are ways to reveal and analyze modular properties in structured data. As the classical modular decomposition is well studied and have an optimal linear-time algorithm, we firstly study the generalizations of these concepts to hypergraphs and present here positive results obtained for three definitions of modular decomposition in hypergraphs from the literature. We also consider the generalization of allowing errors in classical graph modules and present negative results for two this kind of definitions.

The second work focuses on graph data query scenarios. Here the model differs from classical computing scenarios in that we are not designing algorithms to solve an original problem, but we assume that there is an oracle which provides partial information about the solution to the original problem, where oracle queries have time or resource consumption, which we model as costs, and we need to have an algorithm deciding how to efficiently query the oracle to get the exact solution to the original problem, thus here the efficiency is addressing to the query costs. We study the generalized binary search problem for which we compute an efficient query strategy to find a hidden target in graphs. We present the results of our work on approximating the optimal strategy of generalized binary search on weighted trees.

Our third work draws attention to the question of memory efficiency. The setup in which we perform our computations is distributed and memory-restricted. Specif- ically, every node stores its local data, exchanging data by message passing, and is able to proceed local computations. This is similar to the LOCAL/CONGEST model in distributed computing, but our model additionally requires that every node can only store a constant number of variables w.r.t. its degree. This model can also describe natural algorithms. We implement an existing procedure of multiplicative reweighting for approximating the maximum s–t flow problem on this model, this type of methodology may potentially provide new opportunities for the field of local or natural algorithms.

From a methodological point of view, the three types of efficiency concerns cor respond to the following types of scenarios: the first one is the most classical one – given the problem, we try to design by hand the more efficient algorithm; the second one, the efficiency is regarded as an objective function – where we model query costs as an objective function, and using approximation algorithm techniques to get a good design of efficient strategy; the third one, the efficiency is in fact posed as a constraint of memory and we design algorithm under this constraint.

Enumerative and analytic combinatorics

Thursday December 19, 2019, 2PM, Salle 1007

**Sandro Franceschi** (Université Paris-sud) *Invariants de Tutte et Brownien réfléchi dans un cône*

IRIF Cake

Thursday December 19, 2019, 5PM, In front of room 3052

**Gaëtan Douéneau, Daniel Szilagyi** (IRIF Cake^{TM}) *Gâteau de l'IRIF*

^{TM}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.

Higher categories, polygraphs and homotopy

Friday December 20, 2019, 2PM, Salle 1007

**Simon Henry** (Université d'Ottawa) *Les polygraphes homotopiques sont des préfaisceaux*

Dans cet exposé on va étudier une version infini-catégorique de cette construction. On partira d'une monade M fortement cartésienne sur un infini topos, et on construira une infini-catégorie de M-polygraphes. Le cas de la monades infini-catégories strictes agissant sur la catégorie des espaces globulaires donne une version homotopique des polygraphes ordinaires.

On montrera que l'infini-catégorie M-polygraphes a toujours de très bonnes propriétés, qu'on aimerait avoir pour les polygraphes ordinaires mais qui échouent en dimension >2. En particulier les M-polygraphes forment un infini-topos (et si M agit sur une catégorie de préfaisceaux, les M-polygraphes forment une infini-catégorie de préfaisceaux). Si le temps le permet, on montrera comment ces polygraphes homotopiques sont reliés aux polygraphes ordinaires et permettent de déduire des résultats sur les polygraphes ordinaires.