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

Jeudi 27 avril 2017 · 10h30 · Salle 3052

Preuves, programmes et systèmes · Bérénice Delcroix-Oger (Institut de Mathématiques de Toulouse) · Des arbres sans ambiguités

Les tableaux boisés sont des objets combinatoires intervenant notamment dans l'étude de certains modèles de mécanique statistique. Cet exposé porte sur les arbres non ambigus, qui sont un cas particulier de tableaux boisés reliés aux permutations ayant leurs excédences (w(i)>i) en début de mot. Nous avons obtenu, lors d'un travail commun avec J.-C. Aval, A. Boussicault, F. Hivert et P. Laborde-Zubieta, des résultats énumératifs et bijectifs sur ces objets, que je présenterai ici après avoir introduit le cadre de cette étude.

Jeudi 27 avril 2017 · 10h30 · Salle 3052

Combinatoire énumérative et analytique · Bérénice Delcroix-Oger (IMT) · Des arbres sans ambiguités

Jeudi 27 avril 2017 · 14h00 · Salle 3052

Preuves, programmes et systèmes · Jeremy Siek (Indiana University) · The state of the art in gradual typing

Gradual typing is an approach for designing programming languages that integrate static and dynamic type checking. Gradual typing gives the programmer fine-grained control over which regions of a program are statically checked and which regions are dynamically checked. Over the last decade, there has been renewed interest in such an integration partly due to the rise in popularity of dynamic languages. But as small programs grow into large programs, so does the need for early error detection and modularity, which is provided by static type checking. Gradual typing provides a practical migration path for dynamically typed programs to become more statically typed. This talk will give a glimpse at the state of the art in gradual typing. It will describe a) the major challenges in the design and implementation of gradually typed languages, b) the research that has addressed many of of these challenges, and c) the open problems that need to be solved. The research in gradual typing spans both theoretical and practical questions, from mechanized metatheory to efficient compilation.

Vendredi 28 avril 2017 · 14h00 · Salle 1007

Catégories supérieures, polygraphes et homotopie · Martin Szyld · A general limit lifting theorem for 2-dimensional monad theory

Mardi 02 mai 2017 · 14h00 · Salle 1007

Algorithmique distribuée et graphes · Pierre Aboulker (ULB) · TBA

Mardi 02 mai 2017 · 11h00 · Salle 3052

Analyse et conception de systèmes · Joachim Breitner (University of Pennsylvania) · Who needs theorem provers when we have compilers?

After decades of work on functional programming and on interactive theorem proving, a Haskell programmer who wants to include simple equational proofs in his programs, e.g. that some Monad laws hold, is still most likely to simply do the derivation as comments in the file, as all the advanced powerful proving tools are inconvenient.

But one powerful tool capable of doing (some of) these proofs is hidden in plain sight: GHC, the Haskell compiler! Its optimization machinery, in particular the simplifier, can prove many simple equations all by himself, simply by compiling both sides and noting that the result is the same. Furthermore, and crucially to make this approach applicable to more complicated equations, the compiler can be instructed to do almost arbitrary symbolic term rewritings by using Rewrite Rules.

In this rather hands-on talk I will show a small GHC plugin that I can use to prove the monad laws for a non-trivial functor. I am looking forward to a discussion of the merits, limits and capabilities of this approach.

Mardi 02 mai 2017 · 11h00 · Salle 1007

Algorithmes et complexité · Pierre Senellart · Tree decompositions for probabilistic data management

Joint work with Antoine Amarilli, Pierre Bourhis, Mikaël Monet, Silviu Maniu.

In this talk, we review recent work on the problem of efficiently querying probabilistic databases, i.e., compact representations of probability distributions over databases, by exploiting the structure of the data. In the deterministic setting, a celebrated result by Courcelle shows that any monadic second-order query can be evaluated in linear-time on instances of bounded treewidth. We show that this result generalizes to probabilistic instances through the use of provenance. In the probabilistic setting, we show that a bound on the treewidth is necessary for query evaluation to be tractable, in sharp contrast with the deterministic setting. This leads us to studying which real-world databases actually have low treewidth, and to propose practical algorithms for query evaluation in databases that can be partially decomposed in a low-treewidth part and a high-treewidth core.

Pierre Senellart is a Professor in the Computer Science Department at the École normale supérieure in Paris, France, and the head of the Valda team of Inria Paris. He is an alumnus of ENS and obtained his M.Sc. (2003) and Ph.D. (2007) in computer science from Université Paris-Sud, studying under the supervision of Serge Abiteboul. He was awarded an Habilitation à diriger les recherches in 2012 from Université Pierre et Marie Curie. Before joining ENS, he was an Associate Professor (2008–2013) then a Professor (2013–2016) at Télécom ParisTech. He also held secondary appointments as Lecturer at the University of Hong Kong in 2012–2013, and as Senior Research Fellow at the National University of Singapore from 2014 to 2016. His research interests focus around practical and theoretical aspects of Web data management, including Web crawling and archiving, Web information extraction, uncertainty management, Web mining, and intensional data management.

Mercredi 03 mai 2017 · 11h00 · Salle 3052

Séminaire des doctorants · Alexandre Nolin · Quantum, a look through nonlocality

In this talk I will try to give an introduction to the mathematical framework of quantum computing, completely disconnected of the underlying theory of quantum physics. After an exposition of a circuit model for quantum computing, we will split those circuits into two parts (the infamous Alice and Bob) and talk about the behaviours of those bipartite systems, more specifically somewhat counter-intuitive phenomenons like entanglement and nonlocality. Finally, we will see how those phenomenons are relevant in the study of communication complexity, and discuss recent results.

Jeudi 04 mai 2017 · 11h00 · Salle 1007

Combinatoire énumérative et analytique · Svetlana Puzynina (IRIF) · Combinatoire additive basée sur les mots uniformémement récurrents

Un sous-ensemble des entiers strictement positifs est appelé un ensemble IP s'il contient toutes les sommes finies d'une suite infinie croissante d'entiers naturels. Nous étudions les ensembles IP et certaines autres propriétés additives des ensembles d'entiers naturels, avec comme point de vue celui de la combinatoire des mots. Nous utilisons diverses familles bien connues de mots infinis, comme par exemple les mots Sturmiens ou les points fixes de substitution, afin de construire divers ensembles IP possédant une multitude de propriétés additives différentes qui reflètent la richesse de la structure combinatoire du mot sous-jacent.