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

(rafraîchir la page pour changer de notion)


Mihaela Sighireanu (IRIF) is organizing the second edition of SL-COMP, a competition of solvers for separation logic. The final results will be presented at ADSL 2018, a workshop of FLOC2018, which will take place in Oxford on the 13.07.18.
separation logic

Separation logic is a language for describing properties and reasoning about programs that use mutable data structures (i.e. memory cells and pointers). Separation logic has a special support for local reasoning, which is the ability to use and compose properties that involve a subset of the data configuration only: it separates the relevant portion of the data structure from the irrelevant one. Local reasoning gives more compact proofs and specifications for imperative programs than with prior formalisms. Furthermore, it helps with the scalability of proofs done in automatic and semi-automatic verification and program analysis tools.

Mihaela Sighireanu (IRIF) is co-chair of the 18th International Workshop on Automated Verification of Critical Systems (AVOCS) which will take place in Oxford from 18.07.18 to 19.07.18 as part of FLOC2018.


Raphaëlle Crubillé (PhD student IRIF) will present at LICS 2018 an analytic account of the discrete probabilities fragment of a denotational model for higher-order programming with general probabilities, hopefully a first step towards proving that this model is fully abstract.
fully abstract

The quest for a fully abstract model for the contextual equivalence of PCF, a paradigmatic functional language, has been influential in the area of programming languages semantics. A model is fully abstract if it is both sound and complete. A denotational model is complete for a given notion of equivalence between programs if equivalent programs have the same denotation, some mathematical object they are mapped to; it is sound if programs having the same denotation are equivalent.

Berenice Delcroix-Oger (IRIF) participated to the annual festival "Salon Culture & Jeux Mathématiques 2018". On the following video (1:50), she presents a funny game where mathematics help you perform magic tricks!

Amina Doumane

Amina Doumane (former PhD student at IRIF, now at LIP) was awarded the Ackermann prize of EACSL for her PhD thesis entitled On the infinitary proof theory of logics with fixed points.

TYPES 06.06.2018
Delia Kesner (IRIF) and Matthieu Sozeau (IRIF) will both give invited talks entitled “Multi Types for Higher-Order languages” and “The Predicative, Polymorphic Calculus of Cumulative Inductive Constructions and its implementation” at TYPES 2018, held in Braga (Portugal), June 18-21.

IRIF distinguished talk 06.06.2018
We are delighted to host as part of our IRIF Distinguished Talks Series Christos Papadimitriou (Columbia University) on July 13, 10:30 for a talk entitled “A computer scientist thinks about the Brain”.

Software Heritage

Today Roberto Di Cosmo (professor at IRIF) with a ceremony at UNESCO opened to the public the archives of Softwareheritage.org, a worldwide initiative to create a universal library of computer programme source codes since the dawn of the digital age. .


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

Biological algorithm is a term used to describe the biological processes from an algorithmic, or computer scientific, perspective. It concerns questions such as what are the algorithmic challenges faced by the biological organism, and what are the algorithmic principals used in order to overcome these challenges. For example, when a group of ants finds a large piece of food and needs to decide its navigation rout back to the nest, what are the benefits and pitfalls of noise in their communication?

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.

Durant la pause estivale les séminaires ont une activité réduite.