## 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 objectifs scientifiques de l'IRIF se situent au cœur de l'informatique, et plus particulièrement sur la conception, l'analyse, la preuve et la vérification d'algorithmes, de programmes et de langages de programmation. Ils s'appuient sur des recherches fondamentales développées à l'IRIF en combinatoire, graphes, logique, automates, types, sémantique et algèbre.

L'IRIF regroupe près de deux cents personnes. Six de ses membres ont été lauréats de l'European Research Council (ERC), et trois sont membres de l'Institut Universitaire de France (IUF).

## Actualités

*21.05.2018*

Pierre Vial (IRIF) will present at
LICS 2018 an excerpt of his
PhD work at IRIF
proving that every lambda-term has an infinite linear representation in
the infinitary relational model. This work pioneers a technique that
allows giving a semantic even to unproductive programs.

*13.05.2018*

Paul-André Melliès (IRIF) will present at LICS 2018
his work on ribbon tensorial logic, a primary logic designed to reveal the secret topology of reasoning.
This is the first time that logical proofs are faithfully translated into topological
tangles using functorial knot theory.

*11.05.2018*

Amos Korman (IRIF) Amos Korman is co-chairing, and organizing the 6th Workshop on Biological Distributed Algorithms, to be held in London in **July, the 23rd**.

*04.05.2018*

Miklos Santha (IRIF) participates to the conference-debate *« Calcul, communication, simulation et métrologie quantiques : des principes aux réalisations concrètes »* to be held the **15 May** in the Institut de France (23, quai de Conti, 75006 Paris).

*27.04.2018*

IRIF is proud to announce that Delia Kesner,
professor of University Paris Diderot and researcher at IRIF, was appointed senior member of IUF.

*23.04.2018*

Six papers coauthored by IRIF members will be presented at the prestigious conference LICS'18 in
Oxford this summer. Topics range from λ-calculus, to Separation Logic…

*06.04.2018*

Victor Lanvin (PhD student of Giuseppe Castagna, IRIF) is awarded the Google PhD fellowship! Through the FSMP, Google will give a significant support to Victor's research work.

*03.04.2018*

The conference Numeration 2018 will be held on **May 22-25** at the Univerity Paris Diderot, and is organized by Valérie Berthé, Christiane Frougny and Wolfgang Steiner from IRIF.

*28.03.2018*

“The Kappa platform for rule-based modeling”, a collaboration between Jean Krivine (IRIF) and researchers from Harvard University,
ENS and Santa Cruz University will be presented at ISMB2018.

*02.03.2018*

Adrian Kosowski (IRIF), together with Bartek Dudek (University of Wroclaw),
will present at STOC 2018 a new protocol for spreading information
in a population. This is the first time that methods of oscillatory dynamics
are used to solve a basic task of information dissemination.

*27.02.2018*

Constantin Enea (IRIF) is an organizer of the 2018 edition of the
EPIT **research school**, on the subject of software verification, to he held in Aussois on **May 7-11 2018**.

*27.02.2018*

Peter Habermehl (IRIF) and Benedikt Bollig
(LSV, ENS Paris-Saclay) organize the **research school**
MOVEP (*Modelling and Verification of Parallel Processes*), from on **July 16-20** in Cachan.

## Événements

Catégories supérieures, polygraphes et homotopie

vendredi 25 mai 2018, 14h00, Salle 1007

**Martin Szyld** (Université de Buenos Aires) *The homotopy relation in a category with weak equivalences*

I will present the results of the article (arXiv:1804.04244) which deals with the classical construction of the homotopy category of a model category (which is done by performing a quotient of the arrows by the homotopy relation) in the context of categories with weak equivalences. By studying this situation in an abstract context, one can define a relation of homotopy “only with respect to the weak equivalences” which yields the desired localization and coincides with the classical one for model categories. As it is usually the case, the proofs of these results, which consider only a family of arrows instead of three, become simpler. In particular, they allowed a generalization to bicategories in a current work with E. Descotte and E. Dubuc, which I will present too if time permits.

Automates

vendredi 25 mai 2018, 14h30, Salle 3052

**Ulrich Ultes-Nitsche** (University of Fribourg) *A Simple and Optimal Complementation Algorithm for Büchi-Automata*

In my presentation, I am going to present joint work with Joel Allred on the complementation of Büchi automata. When constructing the complement automaton, a worst-case state-space growth of O((0.76n)^n) cannot be avoided. Experiments suggest that complementation algorithms perform better on average when they are structurally simple. We develop a simple algorithm for complementing Büchi automata, operating directly on subsets of states, structured into state-set tuples, and producing a deterministic automaton. Then a complementation procedure is applied that resembles the straightforward complementation algorithm for deterministic Büchi automata, the latter algorithm actually being a special case of our construction. Finally, we prove our construction to be optimal, i.e. having an upper bound in O((0.76n)^n), and furthermore calculate the 0.76 factor in a novel exact way.

Vérification

lundi 28 mai 2018, 11h00, Salle 1007

**Ana Sokolova** (Universität Salzburg, Austria) *Linearizability of Concurrent Data Structures via Order Extension Theorems*

The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Verifying linearizability is a difficult, in general undecidable, problem.

In this talk, I will discuss the semantics of concurrent data structures and present recent order extension results (joint work with Harald Woracek) that lead to characterizations of linearizability in terms of violations, a.k.a. aspects. The approach works for pools, queues, and priority queues; finding other applications is ongoing work. In the case of pools and queues we obtain already known characterizations, but the proof method is new, elegant, and simple, and we expect that it will lead to deeper understanding of linearizability.

Algorithmes et complexité

mardi 29 mai 2018, 11h00, Salle 1007

**Steve Alpern** (University of Wariwick, UK) *Shortest Paths in Networks with Unreliable Directions*

The work of Korman and others, based on investigations of navigational techniques of ‘crazy ants’, leads to the following problem: Let Q be a network with given arc lengths, and let H be a ‘home’ node. At each node a permanent direction is given (one of the adjacent arcs) which leads to a shortest path path from that node to H with probability p less than one. Starting from a node S, a searcher chooses the given direction at each reached node with probability q; otherwise he chooses randomly. He arrives home at node H in expected time T=T(S,H,p,q). How should q be chosen to minimize T? Perhaps when reaching a node the searcher sees its degree k so chooses the given direction with probability q(k). Related problems have been studied for tree from a graph theoretical perspective.

Vérification

vendredi 01 juin 2018, 10h30, 3052

**Derek Dreyer** (Max Planck Institute for Software Systems (MPI-SWS)) *RustBelt: Logical Foundations for the Future of Safe Systems Programming*

Rust is a new systems programming language, developed at Mozilla, that promises to overcome the seemingly fundamental tradeoff in language design between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features.

In this talk, I will present RustBelt (http://plv.mpi-sws.org/rustbelt), the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.

After reviewing some essential features of the Rust language, I will describe the high-level structure of the RustBelt verification and then delve into detail about the secret weapon that makes RustBelt possible: the Iris framework for higher-order concurrent separation logic in Coq (http://iris-project.org). I will explain by example how Iris generalizes the expressive power of O'Hearn's original concurrent separation logic in ways that are essential for verifying the safety of Rust libraries. I will not assume any prior familiarity with concurrent separation logic or Rust.

This is joint work with Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and the rest of the Iris team.

Automates

vendredi 01 juin 2018, 14h30, Salle 3052

**Ines Klimann** (IRIF) *<tba>*

<tba>