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.


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.

A sequent represents a theorem by a sequence of hypotheses and the sequence of possible theses they imply. This formalism underlines a symmetry hypotheses/theses ruled by negation and is used in sequent calculus to formalise proofs and to study their properties.

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.

A part of a program is unproductive if it performs an infinite number of computing steps without any interaction with the rest of the program or external devices. Unproductive code is basically useless, and may even be unsafe, and detecting parts of code that are unproductive is important to improve software quality.

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.


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.

Institut de France

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.


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


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…


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

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


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.
information dissemination

Information dissemination is the process by which a piece of information is propagated in a distributed system through direct communications from node to node. Rumor spreading between humans or broadcasting in a network are two typical examples. Information propagation is a basic building block of many distributed algorithms and its analysis is often critical in understanding their complexity.

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.

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.

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 (, 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 ( 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.

vendredi 01 juin 2018, 14h30, Salle 3052
Ines Klimann (IRIF) <tba>