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.

(Ordonnées par priorité et aléatoire)

Guillaume Chapuy and Enrica Duchi from IRIF coorganize with Christina Goldschmidt (Oxford) the Journées Aléa 2019, a CNRS thematic school about discrete random structures, from 03-18 to 03-22 at CIRM. Register by January 23.

Jeremy Siek

IRIF has the great pleasure to welcome Jeremy Siek, professor at Indiana University Bloomingtom, who is visiting IRIF for five months. Jeremy is the creator of gradual typing and a world-renowed expert in typed programming languages. Meet him in office 4034a.
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.
Amaury Pouly

IRIF has the great pleasure to welcome a new researcher (CNRS), Amaury Pouly, an expert in continuous models of computations, and the analysis and verification of continuous/hybrid dynamical systems.

Pierre Fraigniaud from IRIF organizes the Workshop Complexity and Algorithms (CoA), in the framework of GdR IM, Roscoff, France, April 1-5, 2019. The objective of this workshop is to gather the French community on design and analysis of algorithms, of all forms. Deadlines: submission by 01/02/2019, registration by 02/03/2019.

Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani from IRIF present this week at POPL19 a paper coauthored with Jeremy Siek (Indiana university) about a new formal framework for gradual typing allowing a smoother and more declarative integration of gradual typing in existing programming languages.

Jean-Éric Pin

Jean-Eric Pin, CNRS senior researcher at IRIF, is awarded the Arto Salomaa prize for his outstanding contribution to the field of Automata Theory.


Amélie Gheerbrand and Cristina Sirangelo from IRIF co-organize with L. Libkin, L. Segoufin, and P. Senellart, the 2019 Spring School on Theoretical Computer Science (EPIT) on Databases, Logic and Automata, to happen the 7-12 April 2019 in Marseille. Preregistration before 13 January 2019.

Preuves, programmes et systèmes
Jeudi 24 janvier 2019, 10 heures 30, Ens Lyon
Seminaire Chocola (Ens Lyon) Non encore annoncé.

Gâteau de l'IRIF
Jeudi 24 janvier 2019, 17 heures 30, in front of room 3052
Antoine Allioux, Thomas Colcombet, Chaitanya Leena-Subramaniam, Amaury Pouly (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.

Vendredi 25 janvier 2019, 14 heures 30, Salle 3052
Nathan Grosshans Non encore annoncé.

Lundi 28 janvier 2019, 11 heures, Salle 1007
Mark Batty (University of Kent) A denotational semantics for weak-memory language concurrency with modular DRF-SC

Concurrent languages provide weak semantics: they admit non-sequentially-consistent (SC) behaviour to accommodate weak target architectures and compiler optimisation. Subtle behaviour and intricate specifications result, but two properties help to simplify things – no thin-air values, and DRF-SC. In the first, all values must be computed from constants or inputs to the program, rather than conjured up, for example, through abuse of speculative execution. In DRF-SC, programs without data races are guaranteed SC behaviour. Unfortunately, existing languages like C/C++ admit thin-air values and DRF-SC results only apply to an unrealistic class of programs, excluding systems code and code using concurrency libraries. We provide a modular semantics that avoids thin-air values and we prove a new modular variant of DRF-SC that lifts a key barrier to its usefulness.

Lundi 28 janvier 2019, 11 heures, Salle 3052
Fredrik Dahlqvist (UCL - Department of Computer Science) Semantics of higher-order probabilistic programs with conditioning

We present a denotational semantics for higher-order probabilistic programs in terms of linear operators between Banach spaces. Our semantics is rooted in the classical theory of Banach spaces and their tensor products, but bears similarities with the well-known semantics of higher-order programs à la Scott through the use ordered Banach spaces which allow definitions in terms of fixed points. Being based on a monoidal rather than cartesian closed structure, our semantics effectively treats randomness as a resource.

Algorithmes et complexité
Mardi 29 janvier 2019, 11 heures, Salle 1007
Balthazar Bauer (ENS) An application of communication complexity to cryptography

The hash function are very important primitives in cryptology. To use it, we need to trust the designer. To solve this problem, we can combine several hash functions independently built. But we have to suppose that the designers could communicate. That's why we can reduce the security properties to communication complexity problems. After a presentation of these reductions, we will look in details the communication problems linked to these properties, our knowledge, new results about them. And at the end the open problems that challenge us will be presented.

Mardi 29 janvier 2019, 11 heures, Salle 3052
Giulio Guerrieri (Università di Bologna) Non-idempotent intersection types for call-by-need lambda calculus