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 maître de conférences

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

Prochains séminaires

Mardi 28 février 2017 · 14h00 · Salle 1007

Algorithmique distribuée et graphes · Laurent Viennot (INRIA - IRIF) · Beyond Highway Dimension: Small Distance Labels Using Tree Skeletons

Joint work with Adrian Kosowski

The goal of a hub-based distance labeling scheme for a network $G = (V, E)$ is to assign a small subset $S(u) \subseteq V$ to each node $u \in V$, in such a way that for any pair of nodes $u, v$, the intersection of hub sets $S(u) \cap S(v)$ contains a node on the shortest $uv$-path. The existence of small hub sets, and consequently efficient shortest path processing algorithms, for road networks is an empirical observation. A theoretical explanation for this phenomenon was proposed by Abraham et al. (SODA 2010) through a network parameter they called highway dimension, which captures the size of a hitting set for a collection of shortest paths of length at least $r$ intersecting a given ball of radius $2r$. In this talk, we revisit this explanation, introducing a more tractable (and directly comparable) parameter based solely on the structure of shortest-path spanning trees, which we call skeleton dimension. We show that skeleton dimension admits an intuitive definition for both directed and undirected graphs, provides a way of computing labels more efficiently than by using highway dimension, and leads to comparable or stronger theoretical bounds on hub set size.

Mardi 28 février 2017 · 11h00 · Salle 3052

Sémantique · Ran Chen 1) · Strongly Connected Components in graphs, formal proof of Tarjan1972 algorithm

There is a growing interest in programs proofs checked by computer. Proofs about programs are often very long and have to face a huge amount of cases due to the multiplicity of programs variables and the precise details of the programs. This is very frustrating since we would like to explain the proofs of correctness and publish them in scientific articles. However if one considers simple algorithms, we would expect to explain their proofs of correctness in the same way as we explain a mathematical proof for a non too complex theorem.

We present a human readable and rather intuitive formal proof for the classical Tarjan-1972 algorithms for finding strongly connected components in directed graphs. Tarjan’s algorithm consists in an efficient one-pass depth-first search traversal in graphs which traces the bases of strongly connected components. We describe the algorithm in a functional programming style with abstract values for vertices in graphs, with functions between vertices and their successors, and with data types such that lists (for representing immutable stacks) and sets. We use the Why3 system and the Why3-logic to express these proofs and fully check them by computer.

Vendredi 03 mars 2017 · 10h30 · Amphi Turing

Séminaire de l'IRIF · Joost-Pieter Katoen (RWTH Aachen) · IRIF Distinguished Talks Series: Principles of Probabilistic Programming

Probabilistic programming is en vogue. It is used to describe complex Bayesian networks, quantum programs, security protocols and biological systems. Programming languages like C, C#, Java, Prolog, Scala, etc. all have their probabilistic version. Key features are random sampling and means to adjust distributions based on obtained information from measurements and system observations. We show some semantic intricacies, argue that termination is more involved than the halting problem, and discuss recursion and run-time analysis.

Vendredi 03 mars 2017 · 14h30 · Salle 3052

Automates · Guillaume Lagarde (IRIF) · Non-commutative lower bounds

No knowledge in arithmetic complexity will be assumed.

We still don't know an explicit polynomial that requires non-commutative circuits of size at least superpolynomial. However, the context of non commutativity seems to be convenient to get such lower bound because the rigidity of the non-commutativity implies a lot of constraints about the ways to compute. It is in this context that Nisan, in 1991, provides an exponential lower bound against the non commutative Algebraic Branching Programs computing the permanent, the very first one in arithmetic complexity. We show that this result can be naturally seen as a particular case of a theorem about circuits with unique parse tree, and show some extensions to get closer to lower bounds for general NC circuits.

Two joint works: with Guillaume Malod and Sylvain Perifel; with Nutan Limaye and Srikanth Srinivasan.

Vendredi 03 mars 2017 · 14h00 · Salle 1007

Catégories supérieures, polygraphes et homotopie · Maxime Lucas · Structure simpliciale sur les n-branchements et acyclicité de polygraphes


1) Inria