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)

IRIF is having its back-to-work-day on October 15th. In the morning, there will be a PhD student session, and in the afternoon a series of talks given by new faculty and CNRS members.

Maths en ville

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.


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

ICFP: International Conference On Functional Programming

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

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, 11h00, 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.)

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.

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.