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

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 (DI/ENS) · 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.

Vendredi 05 mai 2017 · 14h30 · Salle 1006

Automates · Sebastián Barbieri (ENS Lyon) · TBA