Institut de Recherche en Informatique Fondamentale (IRIF)


image/svg+xml

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.

Claire Mathieu

27.4.2020
Claire Mathieu (IRIF) has been interviewed by the online news site of CNRS about using graphs to devise a lockdown exit strategy.

Oded Maler Best Paper Award

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.

Accepted paper Eurocomb 2021 - Aubian-Charbit

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.

Sergio Rajsbaum - visitor at IRIF

7.9.2021
IRIF is very pleased to host for three months Sergio Rajsbaum, full time Researcher at the Instituto de Matemáticas of the Universidad Nacional Autónoma de México. This collaboration focuses on the use of algebraic topology to study the complexity of distributed algorithms. Algebraic topology tools have been mainly used for shared memory models. The purpose of the visit is to extend this research to distributed memory models. Professor Rajsbaum is partially funded by an invitational program from École Polytechnique. Meet him in office 4028a.

CONCUR Test-of-Time Award

26.8.2021
Ahmed Bouajjani (IRIF), Javier Esparza, and Oded Maler have received the Concur Test-of-Time Award (period 1996-1999) for their article Reachability Analysis of Pushdown Automata: Application to Model-checking published at CONCUR 1997. Read the interview.

Accepted paper Eurocomb 2021 - Naserasr-Wang

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.

Publication dans PLOS Computational Biology

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.

EUROCOMB 2021 - Three papers coauthored by IRIF PhD students

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.


(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é.

Combinatoire énumérative et analytique
Jeudi 23 septembre 2021, 14 heures, Salle 1007
Séverin Charbonnier (IRIF) Weighted enumeration of ciliated maps and applications

Some models of ribbon graphs can be interpreted as Feynman graphs of matrix models. In this manner, the graphs used by Kontsevich in his proof of Witten's conjecture – about the generating function of intersection numbers of psi-classes satisfying the KdV hierarchy – are Feynman graphs of a cubic hermitian matrix model with external field. Ciliated maps arise as generalisations of those graphs.

I will first describe the ciliated maps and their weighted enumeration. Second, I will detail Tutte's equation and state how the generating functions are computed via topological recursion. Last, I will discuss applications of this result to intersection theory of Witten's class, to the enumeration of fully simple maps and to free probabilities.

In collaboration with Raphaël Belliard, Gaëtan Borot, Bertrand Eynard and Elba Garcia-Failde.

Graph Transformation Theory and Applications
Vendredi 24 septembre 2021, 15 heures, online
Romain Pascual (MICS laboratory, CentraleSupélec, University Paris-Saclay, France) Combinatorial maps: transformations and application to geometric modeling

In the first part of the talk, I will present generalized maps that represent quasi-manifolds through their subdivision into topological cells (vertices,edges, faces, volumes). We defined generalized maps as constrained labeled graphs. Arc labels encode topological relations of the subparts modeled object while node labels describe the geometric data used to represent the object. Modeling operations are designed regardless of the object's underlying topology. Therefore, we generalize DPO rules with a functorial approach to encode semi-global relabeling with a product operation. Rules and their extensions (called rule schemes) are considered valid if any application to a well-formed graph results in an equally well-formed graph. We provide set-theoric conditions on rules and rule schemes to ensure the preservation of the model consistency. In the second part of the talk, I will present how this approach allows the design of geometric modelers (software used to create and edit geometric objects) in Jerboa. The set-theoric conditions can be checked via graph traversal in Jerboa's rule editor to ensure that the code derived from the rule will never break the model. The generated code can be used as an add-on in other software or Jerboa's generic viewer. 

Zoom meeting registration link

YouTube live stream

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.

Manuscript

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.

Manuscript

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