Institut de Recherche en Informatique Fondamentale

IRIF Université Paris 7 CNRS L'IRIF est une unité mixe de recherche (UMR 8243) du CNRS et de l'Université Paris-Diderot, issue de la fusion des deux UMR LIAFA et PPS au 1er janvier 2016.

Ses objectifs scientifiques se déclinent selon trois grandes thématiques au cœur de l'informatique : les fondements mathématiques de l’informatique ; les modèles de calcul et de preuves ; la modélisation, les algorithmes et la conception de systèmes.

Poste de maitre de conférences

Un poste de maitre de conférences est ouvert au concours 2017, affecté à l'IRIF, sur les thématique de l'unité. Consulter la fiche de poste.

Prochains séminaires

Vendredi 20 janvier 2017 · 14h30 · Salle 3052

Automates · Nathanaël Fijalkow (Alan Turing Institute) · Logical characterization of Probabilistic Simulation and Bisimulation.

I will discuss a notion of equivalence between two probabilistic systems introduced by Larsen and Skou in 89 called probabilistic bisimulation.

In particular, I will look at logical characterizations for this notion: the goal is to describe a logic such that two systems are bisimilar if and only if they satisfy the same formulas. This question goes all the way back to Hennessey and Millner for non probabilistic transition systems.

I will develop topological tools and give very general logical characterization results for probabilistic simulation and bisimulation.

Vendredi 20 janvier 2017 · 14h00 · Salle 1007

Catégories supérieures, polygraphes et homotopie · Alexandre Quesney · Opérades Swiss Cheese et décompositions cellulaires

Lundi 23 janvier 2017 · 11h00 · Salle 1007

Vérification · Andrea Cerone (Imperial College London) · Analysing Snapshot Isolation

Snapshot isolation (SI) is a widely used consistency model for transaction processing, implemented by most major databases and some of transactional memory systems. Unfortunately, its classical definition is given in a low-level operational way, by an idealised concurrency-control algorithm, and this complicates reasoning about the behaviour of applications running under SI. We give an alternative specification to SI that characterises it in terms of transactional dependency graphs of Adya et al., generalising serialization graphs. Unlike previous work, our characterisation does not require adding additional information to dependency graphs about start and commit points of transactions. We then exploit our specification to obtain two kinds of static analyses. The first one checks when a set of transactions running under SI can be chopped into smaller pieces without introducing new behaviours, to improve performance. The other analysis checks whether a set of transactions running under a weakening of SI behaves the same as when it running under SI.

Mardi 24 janvier 2017 · 14h00 · Salle 1007

Algorithmique distribuée et graphes · Maximilien Danisch (Telecom Paris Tech) · Towards real-world graph algorithmics

Real-world graphs (a.k.a. complex networks) are ubiquitous: the web, Facebook, Twitter, brain networks, protein interaction networks, etc. Studying these graphs and solving computational problems on them (say maximum clique, partitioning or dense subgraph) has applications in many fields. I will first show that the structure of some real-world graphs is special. In particular, they are not adversarial and some difficult problems (say NP-complete or NP-hard problems) can be solved on some huge real-world graphs (say 2G edges or more). I will then present two works along the lines of “understanding and leveraging the structure of real-world graphs in order to build better algorithms”: (i) Enumerating all k-cliques and (ii) Computing the density-friendly graph decomposition.

Mardi 24 janvier 2017 · 11h00 · Salle 3052

Sémantique · Arnaud Spiwack (Tweag I/O) · Retrofitting linear types

Type systems based on linear logic and their friends have proved that they are both capable of expressing a wealth of interesting abstractions. Among these the ability to mix garbage-collected and explicitly managed data in the same language. This is of prime interest for distributed computations that need to reduce latency induced by GC pauses: a smaller GC heap is a happier GC heap.

I had always had the belief that to add linear types to a language was a rather intrusive procedure and that a language with linear types would basically be an entirely new language. The Rust language is a case in point: it has a linear-like type system, but it's a very different language from your run-of-the-mill functional language.

This turns out not to be the case: this talk presents a way to extend a functional programming language. We are targeting Haskell but there is little specific to Haskell in this presentation. I will focus mostly on the type system and how it can be generalised: among other things the type system extends to dependent types.

Mercredi 25 janvier 2017 · 11h00 · Salle 3052

Séminaire des doctorants · Thibaut Girka (Équipe PPS) · Oracle-based Differential Operational Semantics (or Explaining program differences with programs)

We present a formal framework to characterize differences between deterministic programs in terms of their small-step semantics. This language-agnostic framework defines the notion of /difference languages/ in which /oracles/—programs that relate small-step executions of pairs of programs written in a same language—can be written, reasonned about and composed.
We illustrate this framework by instantiating it on a toy imperative

language and by presenting several /difference languages/ ranging from trivial equivalence-preserving syntactic transformations to characterized semantic differences. Through those examples, we will present the basis of our framework, show how to use it to relate syntactic changes with their effect on semantics, how one can abstract away from the small-step semantics presentation, and discuss the composability of oracles.

Jeudi 26 janvier 2017 · 14h00 · Amphi Darboux - IHP

Combinatoire énumérative et analytique · Sanjay Ramassamy Et Eric Fusy (Brown University et LIX) · “Miquel dynamics for circle patterns” et “Bijections for planar maps with boundaries”