Institut de Recherche en Informatique Fondamentale

Research Institute for Foundations of Computer Science

IRIF Université Paris 7 CNRS IRIF is a research laboratory co-founded by the CNRS and the University Paris-Diderot, resulting from the merging of the two research units LIAFA and PPS on January 1st, 2016.

The scientific objectives of the laboratory are at the core of computer science, focusing on: the mathematical foundations of computer science; computational models and proofs; models, algorithms and system design.

Upcoming seminars

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

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.