L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et de 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, se focalisant sur la conception, l'analyse, la preuve et la vérification d'algorithmes et de programmes, appuyé sur des recherches fondamentales en combinatoire, théorie des graphes, logique, théorie des automates, etc.

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

### Informations pratiques

15.11.2017
IRIF is happy to host and organize the 59th IEEE Symposium on Foundations of Computer Science (FOCS 2018), at Maison de la Chimie, Paris, October 07-09, 2018.

06.10.2017
Guillaume Lagarde and Sylvain Perifel have solved a 20-year old conjecture related to Lempel-Ziv. This will be presented at the 29th ACM-SIAM Symposium on Discrete Algorithms (SODA 2018).

01.09.2017
IRIF has the great pleasure to welcome a new assistant professor: Bérénice Delcroix-Oger, an expert in combinatorics and computational algebra.

15.06.2017
Victor Lanvin wins the first prize for the ACM Student Research Competition Grand Finals, undergraduate category. The prize will be presented on June the 24th at the Turing Award Cerimony in San Francisco.

01.03.2017
The 5-year ERC project CombiTop of Guillaume Chapuy has started on March 1st, 2017. The purpose of this project is to use the ubiquitous nature of certain combinatorial topological objects called maps in order to unveil deep connections between several areas of mathematics.

30.01.2017
Amos Korman has been interviewed by Le Monde for his recent results on ants with several co-autors at IRIF.

15.11.2016
IRIF organizes the 44th ACM Symposium on Principles of Programming Languages (POPL 2017), Jussieu, Paris, January 15-21, 2017.

mercredi 22 novembre 2017 · 11h00 · Salle 3052

Séminaire des doctorants · Jules Chouquet (Proofs and Programs team) · Linear logic proof nets and Taylor expansion.

I will first introduce linear logic proof nets, for the multiplicative and exponential fragment (MELL), and I will especially insist on the computational meaning of the exponential boxes: these are constructions containing the possibility of duplication and deletion of entire parts of the structures (all the non linear part of the calculus).

Once these notions are introduced, I will explain how it is possible to express this computational paradigm in a linear setting through a syntactical Taylor expansion. The idea is to understand exponential boxes in a differential variant of linear logic, and to represent it with linear combination.

If we have time, I will try to give an idea of some algebraic issues concerning this construction, and a method to show for example, that the normal form of the Taylor expansion of a MELL always converges.

NB: Taylor expansion is here analogical to the lambda calculus (with its differential version too) one, if someone heard about it, it can give a first intuition.

jeudi 23 novembre 2017 · 11h45 · Salle 1007

Combinatoire énumérative et analytique · Mathias Lepoutre (École Polytechnique (LIX)) · A bijective proof of the enumeration of maps in higher genus

Bender and Canfield proved in 1991 that the generating series of maps in higher genus is a rational function of the generating series of planar maps. In this talk, I will give the first bijective proof of this result. Our approach starts with the introduction of a canonical orientation that enables us to construct a bijection between $4$-valent bicolorable maps and a family of unicellular blossoming maps.

jeudi 23 novembre 2017 · 10h30 · Salle 3052

Preuves, programmes et systèmes · Simon Castellan (Imperial College) · The parallel intensionally fully abstract model for PCF

In this talk, we introduce a new game semantics framework for concurrency based on event structures, extending the work of Rideau and Winskel. In this framework, we can extend the notions of innocence and well-bracketing to the concurrent (and non-deterministic) case, generalizing the so-called “Abramsky cube”.

This talk focuses on the deterministic case. I will first introduce the concurrent strategies and their composition, in the existing linear setting. I will then present our extension to nonlinearity using copy indices and symmetry to represent uniformity. I will then present our notions of concurrent innocence & well-bracketing, to finish on our result of intensional full abstraction for PCF. Time permitting, I will discuss extensions of this result to non-angelic nondeterminism and probabilities.

vendredi 24 novembre 2017 · 14h30 · Salle 3058

Automates · Paul Brunet (University College London) · tba

lundi 27 novembre 2017 · 14h00 · Salle des Thèses, Halle aux Farines

Soutenance d'habilitation · Stefano Zacchiroli (IRIF) · Large-scale Modeling, Analysis, and Preservation of Free and Open Source Software

mardi 28 novembre 2017 · 10h30 · Salle 3052

Sémantique · Daniela Petrisan (IRIF) · TBA

mardi 28 novembre 2017 · 14h00 · Salle 3052

Analyse et conception de systèmes · Leon Gondelman (Institute for Computation and Information Sciences (Radboud Univ.), Netherlands) · The Spirit of Ghost Code

In the context of deductive program verification, ghost code is part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without any observable difference in the program outcome. In particular, ghost data cannot participate in regular computations and ghost code cannot mutate regular data or diverge. The idea exists in the folklore since the early notion of auxiliary variables and is implemented in many state-of-the-art program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist.

In this talk, we describe a simple ML-style programming language with mutable state and ghost code. Non-interference is ensured by a type system with effects, which allows, notably, the same data types and functions to be used in both regular and ghost code. We define the procedure of ghost code erasure and we prove its safety using bisimulation. A similar type system, with numerous extensions which we briefly discuss, is implemented in the program verification environment Why3.

mardi 28 novembre 2017 · 13h30 · Salle 3052

Vérification · Léon Gondelman (Radboud University, The Netherlands) · The Spirit of Ghost Code

In the context of deductive program verification, ghost code is part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without any observable difference in the program outcome. In particular, ghost data cannot participate in regular computations and ghost code cannot mutate regular data or diverge.

The idea exists in the folklore since the early notion of auxiliary variables and is implemented in many state-of-the-art program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist.

In this talk, we describe a simple ML-style programming language with mutable state and ghost code. Non-interference is ensured by a type system with effects, which allows, notably, the same data types and functions to be used in both regular and ghost code. We define the procedure of ghost code erasure and we prove its safety using bisimulation. A similar type system, with numerous extensions which we briefly discuss, is implemented in the program verification environment Why3.

mercredi 29 novembre 2017 · 14h00 · Salle 1007

Théorie des types et réalisabilité · Guilhem Jaber (ENS Lyon) · A Trace Semantics for System F Parametric Polymorphism

In this talk, we present a trace model for System F that captures Strachey parametric polymorphism. The model is built using operational nominal game semantics and enforces parametricity by using names. This model is used here to prove a conjecture of Abadi, Cardelli, Curien and Plotkin which states that Strachey equivalence implies Reynolds equivalence (i.e. relational parametricity) in System F.