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 deux sont membres de l'Institut Universitaire de France (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.

Numeration 2018

The conference Numeration 2018 will be held on May 22-25 at the Univerity Paris Diderot, and is organized by Valérie Berthé, Christiane Frougny and Wolfgang Steiner from IRIF.


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

IRIF distinguished talk 08.03.2018
In the scope of the IRIF Distinguished Talks Series Monika Henzinger (University of Vienna) will give on April 13 a talk on “The state of the art in dynamic graph algorithms”.


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.


Constantin Enea (IRIF) is an organizer of the 2018 edition of the EPIT research school, on the subject of software verification, to he held in Aussois on May 7-11 2018.


FSMP offers 20 PhD student positions in Maths and TCS under H2020 COFUND project MathInParis. As a member of the FSMP network, IRIF is an eligible hosting lab. Call for application is open until April, 1st 2018. Applicants must be international students, but master students already in France for less than a year are eligible.


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.

Séminaire des doctorants
mercredi 25 avril 2018, 11h00, Salle 3052
Raphaëlle Crubillé (Algebra and calculus, proofs and programs teams) Probabilistic Stable Functions on Discrete Cones are Power Series.

The category of probabilistic coherence spaces (PCoh_!), introduced by Danos and Ehrhard, is a fully abstract model for PCF with *discrete* probabilities, where morphisms can be seen as power series. The category Cstab_m, of measurable cones and measurable stable functions, has been introduced by Ehrhard, Pagani and Tasson as a model for PCF with *continuous* probabilities. In this talk, we will study the shape of stable functions when they are between *discrete* cones, and it will allow us to see that PCoh_! is a full subcategory of Cstab_m.

Théorie des types et réalisabilité
mercredi 25 avril 2018, 14h00, Salle 1007
Hadrien Batmalle (IRIF) Préservation de propriétés du modèle de départ en réalisbilité classique

La réalisabilité classique permet d'interpréter des théories mathématiques classiques, comme la théorie des ensembles ZF, dans divers modèles de calcul (lambda-calcul avec continuations, domaines…) axiomatisés au moyen d'algèbres de réalisabilité. Elle produit ainsi des modèles de ces théories, de même qu'une technique bien connue, le forcing de Cohen, dont elle est en fait une généralisation.

Jusqu'ici, la réalisabilité classique a seulement été étudiée à partir d'un modèle de départ “raisonnable”, supposé au moins valider AC, voire même défini comme l'univers constructible. Dans cet exposé, on étudiera un analogue des “conditions d'antichaîne” du forcing nous permettant d'exporter certaines propriétés du modèle de départ au modèle de réalisabilité; et on l'appliquera pour obtenir des programmes réalisant Non DC (resp. Non CH) à partir de modèles de ZF bien choisis validant Non DC (resp. Non CH).

— DC: axiome du choix dépendant CH: hypothèse du continu

Soutenances de thèses
vendredi 27 avril 2018, 14h00, Salle 1021, Bâtiment Sophie Germain
Alex B. Grilo (IRIF) Quantum proofs, the Local Hamiltonian problem and applications

Manuscript is available here: https://www.irif.fr/~abgrilo/thesis.pdf

Séminaire des doctorants
mercredi 02 mai 2018, 11h00, Salle 3052
Emiliano Lancini (Laboratoire d'Informatique de Paris Nord) Box-Total Dual Integrality and k-Edge-Connectivity

Systèmes complexes
mercredi 02 mai 2018, 14h00, Salle 3052
Mauro Sozio (Telecom Paristech) Fully Dynamic k-center Clustering and Graph Partitioning

Recently, we have witnessed an explosion in the amount of data being readily available to us. This allows us to study and understand the world we live in with unprecedented details. However, the challenges of processing large amounts of data evolving over time are non-trivial. Our talk will start with discussing a few recent results in large-scale graph mining. In particular, we will briefly discuss the main ideas which allowed us to find dense subgraphs in graphs containing up to 20 billion edges. We will then continue our talk presenting a fully dynamic algorithm for k-center clustering, which is the problem of finding a partition of the input data points into k sets with minimum maximum radius. Most of the efforts in developing dynamic data mining algorithms have been focusing on the sliding window model (where at any given point in time only the most recent data items are retained) or more simplistic models. However, in many real-world applications one might need to deal with arbitrary deletions and insertions. For example, one might need to remove data items that are not necessarily the oldest ones, because they have been flagged as containing inappropriate content or due to privacy concerns. Clustering trajectory data might also require to deal with more general update operations.

We develop a (2+epsilon)-approximation algorithm for the k-center clustering problem with “small” amortized cost under the fully dynamic adversarial model. In such a model, points can be added or removed arbitrarily, provided that the adversary does not have access to the random choices of our algorithm. The amortized cost of our algorithm is poly-logarithmic when the ratio between the maximum and minimum distance between any two points in input is bounded by a polynomial, while k and epsilon are constant. Our theoretical results are complemented with an extensive experimental evaluation on dynamic data from Twitter, Flickr, as well as trajectory data, demonstrating the effectiveness of our approach. We conclude our talk with some interesting directions for future work. In particular, we are going to discuss the challenges in developing a fully dynamic algorithm for graph partitioning.