L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université de Paris, qui héberge une équipe-projet 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), cinq sont membres de l'Institut Universitaire de France (IUF), deux sont membres de l'Academia Europæa, et un est membre de l'Académie des sciences.

19.10.2021
Eugene Asarin (IRIF), Alexandre Donzé, Oded Maler, and Dejan Nickovic receive the Test of Time Award at the 21st International Conference on Runtime Verification (RV’21) for their paper Parametric Identification of Temporal Properties. Watch the RV’21 Award Announcement here.

1.9.2021
Three papers coauthored by IRIF Ph.D students will be presented at the European Conference on Combinatorics, Graph Theory and Applications. Topics include oriented graphs, asymmetric hypergraphs and bipartite planar graphs.

3.9.2021
Reza Naserasr and Zhouningxin Wang (IRIF) will present the notion of circular coloring of signed graphs, as a common extension of the circular coloring of graphs and the 0-free coloring of signed graphs. In this work, they consider the problem of finding the best upper bound of the circular chromatic number of restricted families of signed graphs. In particular, they show that every signed bipartite planar graph of negative-girth 6 admits a circular 3-coloring.

3.9.2021
Guillaume Aubian, Pierre Charbit (IRIF) and Pierre Aboulker study the class of oriented graphs such that the out-neighbourhood of any vertex induces a transitive tournament and prove for it a decomposition theorem. As a consequence, they obtain that oriented graphs in this class have dichromatic number at most $2$ and satisfy Caccetta-Häggkvist conjecture.

14.9.2021
Eugene Asarin (IRIF), Thomas Ferrère, Dejan Ničković and Dogan Ulus receive the Oded Maler best paper award in Timed Systems at the conference Formats’2021 for their paper On the complexity of timed pattern matching.

7.10.2021
PPS is holding its journée de rentrée on October 13-14, 2021. This year PPS has 13 new members. The aim of this get-together is to know them and their research topic. Schedule and details of the talks here.

29.9.2021
IRIF researchers are participating to the 30th edition of Fête de la Science. In different schools in Paris, they will be presenting workshops and games related to computer science.

3.9.2021
Reza Naserasr (IRIF) is an invited speaker at the 29th Workshop on Cycles and Colourings. He will present a joint work with Lan Anh Pham (IRIF), Zhouningxin Wang PhD student (IRIF) and Xuding Zhu (University Jinchua): Density of C –4 -critical signed graphs. There is a classic one-to-one correspondence between (2k+1)-colorability of a graph and mapping of a specific subdivision of it to the (2k+1)-cycle. In this work they present an extension of this to 2k-coloring using homomorphisms of signed graphs.

(Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.)

Combinatoire énumérative et analytique
Jeudi 21 octobre 2021, 14 heures, Salle 1007
Florent Koechlin (IRIF, Université de Paris) Séries génératrices et preuves d'intrinsèque ambiguïté

Un langage algébrique est intrinsèquement ambigu si toute grammaire qui le reconnaît est ambiguë, c'est-à-dire qu'elle génère un même mot de deux façons différentes. Décider l'intrinsèque ambiguïté d'un langage algébrique est un problème difficile, indécidable en général. Dans les années 70-80, les preuves d'intrinsèque ambiguïté reposaient essentiellement sur des raisonnements subtils et difficiles sur les arbres de dérivation des grammaires. En 1987, Philippe Flajolet a proposé une nouvelle approche pour montrer que certains langages algébriques sont intrinsèquement ambigus, en montrant que leur série génératrice n'est pas algébrique. Cette approche s'est avérée très efficace : en utilisant cette méthode, Philippe Flajolet a démontré ou redémontré dans son article l'intrinsèque ambiguïté d'une dizaine de langages, dont plusieurs étaient des conjectures de son époque. Dans cet exposé, je propose quelques extensions qui étendent le lien entre la non-ambiguïté des langages et les séries génératrices, et apportent notamment quelques pistes de réponses à deux questions posées par Philippe Flajolet à la fin de son article.

Preuves, programmes et systèmes
Jeudi 21 octobre 2021, 10 heures 15, On-line.
Armaël Guéneau (Aarhus) Program verification on a capability machine in the presence of untrusted code

Catégories supérieures, polygraphes et homotopie
Vendredi 22 octobre 2021, 14 heures, Salle 1007
Antoine Allioux (IRIF) Structures supérieures cohérentes en théorie des types homotopiques

Travail mené conjointement avec Eric Finster et Matthieu Sozeau (https://arxiv.org/abs/2105.00024).

La théorie des types de Martin-Löf peut être vue comme une fondation des mathématiques. Il a été montré que certains de ses modèles validaient une interprétation homotopique des types, ce qui a motivé une nouvelle ligne de développement de celle-ci nommée théorie des types homotopiques.

Dans cette théorie, les types ne sont pas vus comme de simples ensembles car ils ont une structure d'infini-groupoïde non-triviale conférée par leurs types identité. D'où l'idée de formaliser des résultats d'algèbre supérieure en exploitant la structure supérieure des types. Néanmoins, décrire celle-ci de façon interne reste une question ouverte. C'est à dire que l'on peut énoncer des propositions concernant des infini-groupoïdes arbitraires mais que l'on ne sait pas construire une large classe d'infini-groupoïdes, en particulier ceux dont la structure supérieure n'est pas triviale ou tronquée à partir d'une certaine dimension.

Nous proposons une approche consistant à étendre la théorie des types avec un univers de monades polynomiales satisfaisant leurs lois de façon définitionnelle. Cela nous permet de présenter les types et leur structure supérieure, et ainsi d'internaliser un certain nombre de résultats dont le fait que les types sont des infini-groupoïdes.

Automates
Vendredi 22 octobre 2021, 14 heures 30, Salle 3052
Dietmar Berwanger (LSV) Telling Everything. Information Quotients in Games with Communication

We present a model of games with imperfect information that features explicit communication actions, by which a player can send her entire observation history to another player. Such full-information protocols are common in asynchronous distributed systems, here we consider a synchronous setting and cast it as a game on word-automatic trees. The information structures arising from such games are again automatic trees, but their branching degree can be unbounded, and then the synthesis problem becomes challenging. We present a method for constructing a finite bisimulation quotient for a representative subcase, which solves the problem effectively. The construction is a guess; if time allows, we will speculate on how to find such quotients systematically.

The talk is based on joint work (in progress) with Laurent Doyen; a part of the material is presented in [D. Berwanger, L. Doyen (2019): Observation and distinction in infinite games, https://arxiv.org/abs/1809.05978]

Analyse et conception de systèmes
Vendredi 22 octobre 2021, 10 heures 30, Salle 1007
Théo Zimmermann (IRIF) PR of the Month: Architecture of a GitHub bot, the trigger-action model

In the context of the development of the Coq proof assistant, I have created and maintained a multi-function bot to assist developers in automating some basic and repetitive tasks. In this talk, I will present a recent pull request that was submitted to the bot repository and this will be an opportunity to present the way the bot is architectured, and how it uses a modern, typed, GitHub API and suitable OCaml libraries to implement its features, and how that makes it easy to extend.

Sémantique
Mardi 26 octobre 2021, 10 heures 30, Exposé à distance sur Galène – salle 3052 virtuelle
Thomas Ehrhard (CNRS, Université de Paris) Coherent Differentiation [Part 1]

The differential calculus uses addition in a crucial way: this appears clearly in the Leibniz Rule. This is why the differential lambda-calculus as well as differential linear logic feature an unrestricted addition operation on terms (or proofs) of the same type. From an operational point of view, this means that these formalisms feature finite non-determinism. So a natural question arises: is non-determinism inherent to any differential extension of the lambda-calculus and linear logic? Based on intuitions coming from probabilistic coherence spaces, we provide a negative answer to this question, introducing a setting of “summable categories” where the notion of summable pairs of morphisms is axiomatized by means of a functor equipped with three natural transformations satisfying a few axioms. Then we define a notion of differentiation in such a summable category equipped with a resource modality (exponential in the sense of linear logic): this differential structure is a distributive law between a monad associated with the summability structure and the resource comonad, satisfying a few additional axioms. I will present various aspects of this theory (which features similarities with tangent categories), concrete instances of the theory as well as the syntax of a differential version of PCF which can be derived from this general categorical setting. In particular I will show that coherence spaces provide a model of this coherent differentiation, in sharp contrast with differential linear logic.

One world numeration seminar
Mardi 26 octobre 2021, 14 heures 30, Online
Michael Baake (Universität Bielefeld) Spectral aspects of aperiodic dynamical systems

One way to analyse aperiodic systems employs spectral notions, either via dynamical systems theory or via harmonic analysis. In this talk, we will look at two particular aspects of this, after a quick overview of how the diffraction measure can be used for this purpose. First, we consider some concequences of inflation rules on the spectra via renormalisation, and how to use it to exclude absolutely continuous componenta. Second, we take a look at a class of dynamical systems of number-theoretic origin, how they fit into the spectral picture, and what (other) methods there are to distinguish them.