L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris-Diderot, qui héberge deux équipes-projets INRIA.

Les recherches menées à l'IRIF reposent sur l’étude et la compréhension des fondements de toute l’informatique, afin d’apporter des solutions innovantes aux défis actuels et futurs des sciences numériques.

L'IRIF regroupe près de deux cents personnes. Six de ses membres ont été lauréats de l'European Research Council (ERC), trois sont membres de l'Institut Universitaire de France (IUF) et deux sont membres de l'Academia Europæa.

(rafraîchir la page pour changer de notion)

Pierluigi Crescenzi

12.10.2018
IRIF has the great pleasure to welcome a new professor (Paris Diderot): Pierluigi Crescenzi, an expert in graph algorithms, particularly in the analysis of real-world complex networks.

Claire Mathieu

12.10.2018
IRIF has the great pleasure to welcome a new research scientist (CNRS): Claire Mathieu, an expert in algorithms, particularly the design of approximation schemes for NP-hard combinatorial.

IRIF

5.10.2018
IRIF is seeking excellent candidates for about 10 postdoctoral positions in all areas of the Foundations of Computer Science.

Maths en ville

8.10.2018
Jean Krivine (researcher at IRIF) will lead a public debate about Artificial Intelligence at the “Festival Maths en Ville” of Saint-Denis. It will take place on the 11/10/2018 at the theater “L'écran”, starting at 19.30.

ICFP: International Conference On Functional Programming

9.10.2018
The paper “Equivalences for Free : Univalent Parametricity for Effective Transport” of Matthieu Sozeau (IRIF), with his coauthors Nicolas Tabareau and Eric Tanter, has been selected as a distinguished paper of the ICFP conference.

Jean-Éric Pin

7.10.2018
Jean-Eric Pin, CNRS senior researcher at IRIF, is awarded the Arto Salomaa prize for his outstanding contribution to the field of Automata Theory.

Algorithmes et complexité
mardi 16 octobre 2018, 11h30, Salle 1007
Suryajith Chillara (IIT Bombay) A Quadratic Size-Hierarchy Theorem for Small-Depth Multilinear Formulas

It is a fundamental problem in the study of computational complexity to understand if access to more resources would mean strictly more computational power. In classical complexity, we have seen such examples in terms of Time Hierarchy and Space Hierarchy theorems. Here, time and space are the resources. It is natural to ask such a question in the setting of algebraic complexity setting. Here, access to more resources translates to allowing the model to perform more number of operations which in turn is allowing the “algebraic formulas” to have larger size.

Arithmetic formulas are directed trees where the leaves are labelled by variables and elements of the field, and internal vertices are labelled by + or x. Every internal vertex computes a polynomial by operating on its inputs. It is easy to see that they are a natural model of computation of polynomials, syntactically (symbolically). The size of the arithmetic formulas refers to the number of + and x operations needed to compute the polynomial.

Rephrasing the question in the algebraic setting we ask the following: for any s, \varepsilon >0, are there polynomial computations that can be efficiently computed by arithmetic formulas of size s but not by any arithmetic formula of size s^{1-\varepsilon}?

In this talk, we will restrict ourselves to arithmetic formulas where computation at every vertex is a multilinear polynomial and here we show explicit separations between the expressive powers of multilinear formulas of small-depth and all polynomial sizes. The multilinear restriction is a reasonable one since most polynomials of interest are indeed multilinear.

Formally, we will show that for any s = poly(n) and \delta > 0, we show that there are explicit polynomial families that have multilinear formulas of size at most s but no 'small'-depth multilinear formulas of size less than s^{0.5 - \delta}. Our proof can be viewed as a derandomization of a lower bound technique of Raz (JACM 2009) using \epsilon-biased spaces.

(Joint work with Nutan Limaye and Srikanth Srinivasan. Appeared in the proceedings of ICALP 2018.)

Sémantique
mardi 16 octobre 2018, 10h30, Salle 3052
Thomas Ehrhard (IRIF) Une remarque sur les espaces cohérents probabilistes et la distance opérationnelle entre les programmes

On utilise les régularités des morphismes de la catégorie cartésienne fermée des espaces cohérents probabilistes pour majorer une distance naturelle sur les (classes d'équivalence observationnelle) de termes de PCF probabilistes par une distance définissable dans le modèle.

Séminaire des doctorants
mercredi 17 octobre 2018, 11h00, Salle 3052
Abishek De Et Simon Mauras () Newcomers' session

Abishek De : Distributed Control Problem for Free Choice Systems

The distributed synthesis problem is about constructing correct distributed systems, i.e., systems that satisfy a given specification. We consider a slightly more general problem of distributed control, where the goal is to restrict the behavior of a given distributed system in order to satisfy the specification. Our systems are finite state machines that communicate via rendezvous (asynchronous automata). There are a few classes of systems for which the problem has been shown decidable. We solve it for free choice systems, systems whose entire behaviour can be expressed in a (possibly infinite) tree.


Simon Mauras : Social choice theory, and a small survey about rank aggregation

How should we vote? This question has been adressed by philosophers and mathematicians since the XVIIIth century, but no satisfactory solution exists. The talk will start with classical results on social choice theory and move on to the aggregation of rankings seen as an optimization problem. We will discuss NP-Hardness, Hardness of approximation and Approximation algorithms for several variants of this problem.

Combinatoire énumérative et analytique
jeudi 18 octobre 2018, 11h45, Salle 1007
Isaac Konan (IRIF) Combinatoire autour des identités de type Rogers-Ramanujan

“Pour un entier positif n donné, on dénombre autant de partitions de n en parts distinctes que de partitions de n en parts impairs”.

Cette identité, attribuée à Euler, résume bien ce qu'est une identité du type Rogers-Ramanujan: une égalité entre cardinaux d'ensembles de partitions, qui pour l'un vérifient des conditions de congruences sur ses parts, et l'autre des conditions sur les différences entre parts consécutives.

Nous présenterons certaines méthodes utilisées pour établir ces égalités, telles que la méthode des mots pondérés, les équations de q-différence, ainsi que des bijections directes. On étudiera entre autre l'identié Alladi-Gordon qui généralise celle de Schur, et si le temps nous le permet, l'identité de Siladic issue de la théorie des représentations des algèbres de Lie.

Soutenances de thèses
vendredi 19 octobre 2018, 09h30, Salle 580F (salle des thèses), Bâtiment Halle aux Farines
Marie Kerjean (IRIF) Reflexive spaces of smooth functions: a logical account for linear partial differential equations

Around the Curry-Howard correspondence, proof-theory has grown along two distinct fields: the theory of programming languages, for which formulas acts as data types, and the semantic study of proofs. The latter consists in giving mathematical models of proofs and programs. In particular, denotational semantics distinguishes data types which serves as input or output of programs, and allows in return for a finer understanding of proofs and programs. Linear Logic (LL) gives a logical interpretation of the basic notions of linear algebra, while Differential Linear Logic allows for a logical understanding of differentiation.

This manuscript strengthens the link between proof-theory and functional analysis, and highlights the role of linear involutive negation in DiLL. The first part of this thesis consists in an overview of prerequisites on the notions of linearity, polarisation and differentiation in proof-theory, and gives the necessary background in the theory of locally convex topological vector spaces. The second part uses two standard topologies on the dual of a topological vector space and gives two models of DiLL: the weak topology allows only for a discrete interpretation of proofs through formal power series, while the Mackey topology on the dual allows for a smooth and polarised model of DiLL. Finally, the third part interprets proofs of DiLL by distributions. We detail a polarized model of DiLL in which negatives are Fr\'echet Nuclear spaces, and proofs are distributions with compact support. We show that solving linear partial differential equations with constant coefficients can be typed by a syntax similar to the one of DiLL, which we detail.

Catégories supérieures, polygraphes et homotopie
vendredi 19 octobre 2018, 14h00, Salle 1007
Muriel Livernet (IMJ) Suites spectrales et équivalences faibles

Depuis leur introduction par Leray dans les années 50 les suites spectrales sont devenues essentielles dans beaucoup de domaines mathématiques comme outil de calculs homologiques et homotopiques. Parmi les sources importantes de suites spectrales on trouve les complexes filtrés et les bicomplexes. On introduit pour chacune de ces catégories la notion de E_r-quasi-isomorphisme, liée à la r-ième page des suites spectrales associées aux objets considérés. On montrera dans cet exposé, une fois toutes les notions utiles définies (y compris les structures de catégorie modèles) que les catégories des complexes filtrés et des bicomplexes admettent des structures de catégorie modèle au sens de Quillen, où les équivalences faibles sont les E_r-quasi-isomorphismes.

Ceci est un travail en commun avec: Joana Cirici, Daniela Egas-Santander et Sarah Whitehouse.

Automates
vendredi 19 octobre 2018, 14h30, Salle 3052
Andrew Rizhikov (University Paris-Est Marne-la-Vallée) Finding short synchronizing and mortal words for prefix codes

We study approximation algorithms for two closely related problems: the problems of finding a short synchronizing and a short mortal word for a given prefix code. Roughly speaking, a synchronizing word is a word guaranteeing a unique interpretation, and a mortal word is a word guaranteeing no interpretation for any sequence of codewords. We concentrate on the case of finite prefix codes and consider both the cases where the code is defined by listing all its codewords and where the code is defined by an automaton recognizing the star of the code. This is a joint work with Marek Szykuła (University of Wroclaw).

Vérification
lundi 22 octobre 2018, 11h10, Salle 1007
Marie Fortin (LSV - ENS Paris-Saclay) It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with “Happened Before”

Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport's happened-before relation. We introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.

This is joint work with Benedikt Bollig and Paul Gastin, presented at CONCUR’18.