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 recherches menées à l'IRIF reposent sur l’étude et la compréhension des fondements de toute l’informatique, afin d’apporter des solutions innovantes aux défis actuels et futurs des sciences numériques.

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

(rafraîchir la page pour changer de notion)


IRIF is seeking excellent candidates for about 10 postdoctoral positions in all areas of the Foundations of Computer Science.

Distinguished Talk

We are delighted to host as part of our IRIF Distinguished Talks Series Maurice Helihy (Brown University) on Nov. 16, 10:30 for a talk entitled “Atomic Cross-Chain Swaps”.


IRIF and PCQC are partners in the EU Flagship project Quantum Internet Alliance (QIA) and in charge of delivering the QIA's blueprint for the future of quantum communications. The EU selected nineteen research projects, and ten of them are based on French teams.

Graph Theory in Paris

The first session of a series of seminars Graph Theory in Paris will be hosted by IRIF. There will be two seminars by Monique Laurent and Lex Schrijver on November 23, at 2pm, in Amphi Turing of Sophie Germain building.

The first meeting of the French-Chinese research project “Verification Interaction Proof” will take place in Paris at IRIF on November 19 - 24. Registration is free but mandatory.

Adrien Guatto

IRIF has the great pleasure to welcome a new assistant professor (Paris Diderot): Adrien Guatto, an expert in synchronous languages, temporal logic and categorical semantics.

Daniela Petrisan

IRIF has the great pleasure to welcome a new assistant professor (Paris Diderot): Daniela Petrisan, an expert in categories, co-algebra and automata.


The last plenary meeting of GDRI Logique Linéaire will take place at IRIF, December 3-5. The program will consist of talks given by members of the GDRI.

Combinatoire énumérative et analytique
jeudi 15 novembre 2018, 11h45, Salle 1007
Frédéric Meunier (ENPC) Envy-free division of a cake: the poisoned case, and other variations

Given a cake (identified with the interval [0,1]) and players with different tastes, the envy-free cake-cutting problem asks for a partition of the cake into connected pieces so that it is possible to assign the pieces to the players without making any of them jealous. The Stromquist-Woodall theorem ensures the existence of such an envy-free division under mild conditions. Recently, Segal-Halevi asked whether these conditions could be even further relaxed by allowing that some players dislike the cake (e.g., they know the cake has been poisoned). In the traditional setting, all players are “hungry”, and always prefer to get something instead of nothing. We provide a partial answer to that question and propose also other extensions, e.g., when suddenly one player disappears.

Based on joint work with Florian Frick, Kelsey Houston-Edwards, Francis E. Su, Shira Zerbib.

Gâteau du jeudi - Thursday Cake
jeudi 15 novembre 2018, 17h30, in front of room 3052
Kostia Chardonnet, Jonas Landman, Laurent Pietroni (IRIF CakeTM) Gâteau de l'IRIF

IRIF CakeTM is an amazing opportunity to meet people while simultaneously eating cakes baked by your fellow colleagues! Join us every Thursday, at 5pm, in front of room 3052 (Sophie Germain 3rd floor) for a weekly feast. You can also express your cooking skills and volunteer to bake a cake by sending an email to cake@irif.fr.

Preuves, programmes et systèmes
jeudi 15 novembre 2018, 11h00, Salle 3052 + Amphi Turing + 1016
Eric Tanter, Flavien Breuvart, Shane Mansfield & Xavier Leroy (Chocola meeting in Paris) Salidou's day

11:00 – 12:30 Éric Tanter (Universidad de Chile & Inria Paris) - Invited talk: Abstracting Gradual Typing: Principles and Application to Gradual Parametricity

  Gradual typing enables programming languages to seamlessly combine dynamic and static checking. Language researchers and designers have extended a wide variety of type systems to support gradual typing. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs. Based on an understanding of gradual types as abstractions of static types, we have developed systematic foundations for gradual typing based on abstract interpretation, called Abstracting Gradual Typing (AGT for short). Gradual languages designed with the AGT approach satisfy, by construction, the established criteria for gradually-typed languages. In this talk, I will give a brief introduction to AGT in a simply-typed setting, and will then discuss recent work on a gradual counterpart of System F that enforces relational parametricity, even in the presence of imprecise types.

14:00 – 15:00 Flavien Breuvart (Université Paris 13) - Invited talk: Graded Types Parametricity : Principles and Application to Abstract Interpretation

  In this talk, we will briefly present the yet-to-start project CoGITARe, which aims at developing further graded types expressivity and inference in order to use them to perform abstract interpretations.
  In a second time, we give an historic on graded type systems and their expressivity. Then, we will see that this expressivity is limited by a lake of dependency/parametricity. We will thus explore two ongoing research directions that adds two very different kind of parametricity to graded types.
  (The provocative title should only be taken as a joke. Despite their apparent similitudes, this work and Éric Tanter's have vastly different objectives and involved different issues and techniques. In particular, notice that gradual and graded types are fundamentally different.)

15:30 – 16:30 Shane Mansfield (Univ. of Oxford) - Invited talk: An overview of empirical models

  Empirical models are a way of formalising data that arises in physical experiments. They were first proposed by Abramsky and Brandenburger as part of a framework to analyse fundamentally non-classical phenomena in quantum systems. Conveniently from a computer science perspective, they abstract away from the mathematical baggage of quantum theory and instead allow the key phenomena to be characterised purely as features of empirical data. After introducing the basic framework I will discuss some more recent results and developments, drawing on joint work with a number of collaborators. In particular: quantum computations can simply be modelled as classical computations with the additional ability to interact with a resource empirical model; quantitative measures of non-classicality can be shown to relate directly to some basic quantum-over-classical computational advantages; and the beginnings of a category-theoretic approach to reasoning about empirical models have emerged.

18:00 – 19:00 Xavier Leroy - Lecture: Leçon inaugurale au Collège de France

  This is not part of the CHoCoLa day, but you might be interested in attending! See https://www.college-de-france.fr/site/xavier-leroy/inaugural-lecture-2018-11-15-18h00.htm
  The meeting will take place in Bâtiment Sophie Germain, here.
  We will first gather at the 3rd floor of the building, for a breakfast.
  We will then move for the talk of the morning (11.00-12.30) to Amphi Turing.
  We will have lunch in room 3052
  In the afternoon (14h-16h30), we will be in room 1016

Séminaire de l'IRIF
vendredi 16 novembre 2018, 10h30, Amphithéâtre Pierre-Gilles de Gennes, Bât. Condorcet
Maurice Herlihy (Brown University) IRIF Distinguished Talks Series: Atomic Cross-Chain Swaps

An atomic cross-chain swap is a distributed coordination task where multiple parties exchange assets across multiple blockchains, for example, trading bitcoin for ether. An atomic swap protocol guarantees (1) if all parties conform to the protocol, then all swaps take place, (2) if some coalition deviates from the protocol, then no conforming party ends up worse off, and (3) no coalition has an incentive to deviate from the protocol. A cross-chain swap is modeled as a directed graph D, whose vertexes are parties and whose arcs are proposed asset transfers. For any pair (D,L), where D=(V,A) is a strongly-connected directed graph and L⊂V a feedback vertex set for D, we give an atomic cross-chain swap protocol for D, using a form of hashed timelock contracts, where the vertexes in L generate the hashlocked secrets. We show that no such protocol is possible if D is not strongly connected, or if D is strongly connected but L is not a feedback vertex set.

vendredi 16 novembre 2018, 14h30, Salle 358
Manon Stipulanti (Université de Liège) A way to extend the Pascal triangle to words

The Pascal triangle and the corresponding Sierpinski gasket are well-studied objects. They exhibit self-similarity features and have connections with dynamical systems, cellular automata, number theory and automatic sequences in combinatorics on words. In this talk, I will first recall the well-known link between those two objects. Then I will exploit it to define Pascal-like triangles associated with different numeration systems, and their analogues of the Sierpinski gasket. This a work in collaboration with Julien Leroy and Michel Rigo (University of Liège, Belgium).

Gâteau du jeudi - Thursday Cake
jeudi 22 novembre 2018, 17h30, in front of room 3052
Cédric Ho Thanh, Alessandro Luongo, Axel Osmond, Anupam Prakash, Matthieu Sozeau (IRIF CakeTM) Gâteau de l'IRIF

IRIF CakeTM is an amazing opportunity to meet people while simultaneously eating cakes baked by your fellow colleagues! Join us every Thursday, at 5pm, in front of room 3052 (Sophie Germain 3rd floor) for a weekly feast. You can also express your cooking skills and volunteer to bake a cake by sending an email to cake@irif.fr.

Preuves, programmes et systèmes
jeudi 22 novembre 2018, 10h30, Salle 3052
Stéphane Graham-Lengrand (CNRS & École Polytechnique) TBA

Combinatoire énumérative et analytique
jeudi 22 novembre 2018, 11h45, Salle 1007
Arthur Nunge (IRIF) TBA

Preuves, programmes et systèmes
jeudi 22 novembre 2018, 10h30, Salle 3052
Stéphane Graham-Lengrand (LIX, CNRS) The intuitionistic calculus that was discovered 6 times

In this talk I will review G4ip, a simple calculus for intuitionistic propositional logic (IPL) that provides a decision procedure for provability. Its basic mechanisms can be traced back to Vorob'ev in the 50s, and were found again by Hudelmaier (88), Dyckhoff (90), Paulson (91), and (with a linear logic flavour) Lincoln-Scedrov-Shankar (91). In 2015, Claessen and Rosén presented the fastest decision procedure for IPL, based on SMT-solving techniques. We describe their algorithm and show how it can be seen as a variant of the aforementioned calculus, albeit with key variations that provide increased performance. Their algorithm relies on a SAT-solver used as a black box and treats intuitionistic entailment as a theory. We show how the recent framework of model-constructing satisfiability for SMT-solving could further integrate intuitionistic reasoning within the main SAT-solving loop. This would constitute an intuitionistic variant of the main algorithm of SAT-solvers, where Kripke models are built instead of Boolean models.