## 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 scientific objectives of IRIF are at the core of computer science and, in particular, they focus on the conception, analysis, proof, and verification of algorithms, programs, and programming languages. They are built upon fundamental research activities developed at IRIF on combinatorics, graphs, logics, automata, type, semantics, and algebras.

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 Europaea.

## News

*25.05.2018*

Marie Kerjean (PhD student IRIF) will present at
LICS 2018
a logical account for linear partial differential equations.
With this work, she unveils a bridge between mathematical physics and proof theory,
paving the way for exciting and mutually beneficial transfers of techniques.

*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*
organized by **Académie des sciences** at the Institut de France on ** May 15**.

*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 on gradual typing.

*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*

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.

## Events

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>