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.

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.

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.

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.

30.8.2021
El Mehdi Cherradi (IRIF) and Paul-André Melliès (IRIF) will present at Category Theory Conference 2021 their work on derivators, a clever tool introduced by Grothendieck to compute homotopy limits and colimits of spaces, exploring the idea that derivators should be understood as generalised categories.

27.8.2021
Claire Mathieu (IRIF) et ses collaborateurs publient les résultats de leur recherche Mitigating COVID-19 outbreaks in workplaces and schools by hybrid telecommuting dans le journal PLOS Computational Biology. Cet article l'impact de deux stratégies, dites de rotation et d’alternance, pour freiner l’épidémie de Covid-19 que ce soit dans une école ou un bureau. Lire l'article complet ici et le communiqué de presse du CNRS ici.

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
Yiting Jiang (IRIF) and Jaroslav Nešetřil will present a result that there are infinitely many minimal asymmetric k-uniform hypergraphs.

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.

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

Nombre limité d'évènements durant les vacances d'été.

Vérification
Lundi 27 septembre 2021, 11 heures, 1007 and Zoom link
Paula Herber (University of Münster) Contract-based Verification of Hybrid Simulink Models with Differential Dynamic Logic

Cyber-physical systems, where digital components interact with a physical environment, are ubiquitous in our everyday lives. Digital devices assist our households, monitor our health, and support our transportation in airplanes, trains, or cars. While the complexity of cyber-physical systems is steadily increasing, a failure in such systems can have serious consequences. Model-driven development provides an approach to cope with the increasing complexity, but has the serious drawback that industrially used modeling languages, such as Matlab/Simulink, have only informally defined semantics. To overcome this problem, we propose to precisely capture the semantics of hybrid Simulink models with an automated transformation into the formally well-defined differential dynamic logic (dL). Our transformation enables us to formally verify crucial safety properties of hybrid Simulink models with the interactive theorem prover KeYmaera X. KeYmaera X enables deductive reasoning and thus has the potential to scale well even for larger systems. However, the interactive verification with KeYmaera X is still expensive in terms of manual effort and required expertise. To reduce the verification effort, we propose to define /hybrid contracts/, which enable compositional verification, but still have to be defined manually. In this talk, I will summarize our transformation from Simulink to dL, hybrid contracts for compositional verification, and then discuss the idea of using /hybrid contract patterns/ to ease the interactive verification of cyber-physical systems with KeYmaera X.

Soutenances de thèses
Lundi 27 septembre 2021, 15 heures, Online via Zoom
Zeinab Galal (IRIF) Bicategorical orthogonality constructions for linear logic

This thesis is concerned with the bicategorical semantics of linear logic. We are specifically interested in the categorification of the relational model of linear logic with the generalized species model introduced by Fiore, Gambino, Hyland and Winskel; and its refinements using orthogonality constructions. We first present a bicategorical generalization of the model of finiteness spaces introduced by Ehrhard. We introduce an orthogonality construction on the bicategory of profunctors based on finite presentability to obtain a new bicategory where all interactions are enforced to be finite. We then consider the categorication of the computational notion of sta- bility from stable functions to stable functors. We bring together generalized species of structures and stability by refining the species model with an or- thogonality on subgroups of endomorphisms for each object in a groupoid. We show that this orthogonality allows us to restrict the analytic functors to stable functors and prove that they form a cartesian closed bicategory. We lastly study the categorification of the qualitative Scott model of linear logic and its connection with the quantitative species model of Fiore et al. We start by showing that the bicategory of profunctors with the finite coproduct pseudo-comonad is a model of linear logic that categorifies the Scott model. We then define an orthogonality between the Scott bicategory and the species bicategory that allows us to construct a new bicategory giving us a first step towards connecting linear and non-linear substitution in this setting.

Soutenances de thèses
Mardi 28 septembre 2021, 15 heures, Salle 3052 & Zoom
Chaitanya Leena Subramaniam (IRIF) From dependent type theory to higher algebraic structures

In the first part of this dissertation, we give a definition of “dependently typed/sorted algebraic theory”, generalising the ordinary multisorted algebraic theories of Lawvere–Bénabou. Dependently sorted algebraic theories in our sense form a strict subclass of the “generalised algebraic theories” of Cartmell. We prove a classification theorem for dependently sorted algebraic theories, and use this theorem to prove the existence of dependently sorted algebraic theories for a number of varieties of algebraic structures, such as small categories, n-categories, strict and weak omega-categories, planar coloured operads and opetopic sets. We also prove a Morita equivalence between dependently sorted algebraic theories and essentially algebraic theories, showing that every locally finitely presentable category is the category of models of some dependently sorted algebraic theory. We give a definition of strict and weak homotopical models of a dependently sorted algebraic theory, and prove a rigidification theorem in a particular case. We also study the opetopic case in detail, and prove that a number of varieties of algebraic structures such as small categories and coloured planar operads can be “typed” by the category of opetopes.

The second part of this dissertation concerns accessible reflective localisations of locally presentable infinity-categories. We give a definition of “pre-modulator”, and prove a canonical correspondence between pre-modulators and accessible orthogonal factorisation systems on a locally presentable infinity-category. Moreover, we show that every such factorisation system can be generated from a pre-modulator by a transfinite iteration of a “plus-construction”. We give definitions of “modulator” and “left exact modulator”, and prove that they correspond to those factorisation systems that are modalities and left-exact modalities respectively. Finally we obtain a correspondence between left-exact localisations of infinity-topoi and left-exact modulators.

One world numeration seminar
Mardi 28 septembre 2021, 14 heures 30, Online
Philipp Hieronymi (Universität Bonn) A strong version of Cobham's theorem

Let k,l>1 be two multiplicatively independent integers. A subset X of N^n is k-recognizable if the set of k-ary representations of X is recognized by some finite automaton. Cobham’s famous theorem states that a subset of the natural numbers is both k-recognizable and l-recognizable if and only if it is Presburger-definable (or equivalently: semilinear). We show the following strengthening. Let X be k-recognizable, let Y be l-recognizable such that both X and Y are not Presburger-definable. Then the first-order logical theory of (N,+,X,Y) is undecidable. This is in contrast to a well-known theorem of Büchi that the first-order logical theory of (N,+,X) is decidable. Our work strengthens and depends on earlier work of Villemaire and Bès.

The essence of Cobham's theorem is that recognizability depends strongly on the choice of the base k. Our results strengthens this: two non-Presburger definable sets that are recognizable in multiplicatively independent bases, are not only distinct, but together computationally intractable over Presburger arithmetic.

This is joint work with Christian Schulz.

Combinatoire énumérative et analytique
Jeudi 30 septembre 2021, 10 heures 30, IHP
Seminaire Flajolet (IHP) Valentin Feray, Marc Lelarge, Irene Marcovici

Catégories supérieures, polygraphes et homotopie
Vendredi 1 octobre 2021, 14 heures, Salle 1007
El Mehdi Cherradi (IRIF) Dérivateurs de Quillen et doubles catégories

Étant donnée une catégorie avec une notion d'homotopie, par exemple une catégorie relative, la notion de dérivateur introduite par Grothendieck permet de décrire les catégories de diagrammes à homotopie près, et les relations fonctorielles qu'elles entretiennent.

Dans cet exposé, nous étudierons comment le prédérivateur associé à une telle catégorie relative se restreint en un objet simplicial dans la catégorie CAT des catégories (non nécessairement petites). Cet objet simplicial peut être vu comme un “nerf homotopique” qui décrit les chemins de longueurs n dans la catégorie d'origine, vus à homotopie près.

Partant de ces observations, nous montrerons que dans le cas d'une catégorie de modèle, l'objet simplicial satisfait une condition de Segal, et définit pour cette raison une double catégorie. Cette double catégorie peut être vue comme combinant en une seule structure la catégorie de modèle d'origine (horizontalement) et sa catégorie homotopique (verticalement).

Nous montrons aussi que la construction précédente est compatible avec la structure de dérivateur établie par Cisinski pour un prédérivateur associé à une catégorie de modèle : on obtient ainsi un nouveau dérivateur prenant ses valeurs dans la catégorie DblCAT des doubles catégories plutôt que dans CAT.

Automates
Vendredi 1 octobre 2021, 14 heures 30, Salle 3052
Jacques Sakarovitch (IRIF, CNRS & Télécom Paris) Derived terms without derivation

The topic of this talk is, once again, the transformation of rational expressions into finite automata, a much laboured subject. In our last joint work, Sylvain Lombardy and I take a shifted perspective on the derivation of expressions method (due to Brzozowski and Antimirov) which reveals that there is indeed no derivation involved. This broadens the scope of the method to expressions over non free monoids.