## Bienvenue

L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris Cité, 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), six 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.

## Notion du jour

## Actualités

*10.3.2023*

Les prochaines Journées Nationales du GDR IM (JNIM 2023) auront lieu à l'Université Paris Cité du **4 avril au 7 avril** et sont organisées par l'IRIF. Programme et inscription ici.

*7.3.2023*

The paper “Decentralized Asynchronous Crash-resilient Runtime Verification” authored by Borzoo Bonakdarpour (MSU), **Pierre Fraigniaud (IRIF)**, Sergio Rajsbaum (UNAM), David Rosenblueth (UNAM), and Corentin Travers (LIS) has been selected in the “sample of [eight] exciting [..] articles on a diverse range of topics that were published in 2022” in the **Journal of the ACM (JACM)**.

*6.3.2023*

**Farzad Jafarrahmani**, former PhD student at IRIF explains his thesis Fixpoints of Types in Linear Logic from a Curry-Howard-Lambek Perspective in this written interview.

*6.3.2023*

**“Manuel de Cryptanalyse à l’usage de la NSA”** est une conférence ludique, présentée par **Sylvain Perifel – Maître de conférences (Université Paris Cité/IRIF)** à l’occasion de l’édition 2022 de la Fête de la Science. Elle retrace et met en pratique les différentes avancées historiques de cette science, du **code de César à RSA** en passant par les **substitutions mono-alphabétiques** et par le **chiffre de Vigenère**.

*27.2.2023*

**Shared engineer position in formal methods**, between **IRIF**, LIPN and LMF. Deadline to apply: **17/03/2023**.

*7.3.2023*

Pour la troisième année consécutive, la **Faculté des Sciences d’Université Paris Cité** lance un appel à manifestation d’intérêt pour accompagner et soutenir ses membres dans leurs initiatives ayant vocation à rendre accessible un sujet de recherche scientifique à un public non spécialiste. **Date limite 20 mars 2023 minuit.**

*6.3.2023*

**Abhishek De**, former PhD student at IRIF explains his thesis "Linear logic with the least and greatest fixed points. Truth semantics, complexity and a parallel syntax in this written interview.

*27.2.2023*

One paper authored by IRIF member will be presented at STOC 2023, **June 20-23, 2023** in Orlando, Florida.

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

## Agenda

Algorithmes et structures discrètes

Mercredi 22 mars 2023, 15 heures, 3052

**Michail Lampis** (LAMSADE) *First Order Logic on Pathwidth Revisited Again*

In this talk we take a high-level view of this area of research and survey results that attempt to improve upon this performance by considering more restricted classes of inputs. This is known to be impossible, even if we restrict the input to graphs of treewidth 1 (trees) and only consider FO logic; or if we consider graphs of pathwidth 1 (caterpillars) and consider MSO logic. This would seem to indicate that Courcelle's theorem is “best possible”. Surprisingly, we discover that in the only remaining case which has so far been overlooked, namely FO logic on graphs of constant pathwidth, all known hardness results fail, because the problem becomes tractable with an elementary parameter dependence on the input formula. Our result generalizes previously known meta-theorems for the much more restricted parameter tree-depth.

Results based on a preprint available here: https://arxiv.org/abs/2210.09899

Preuves, programmes et systèmes

Jeudi 23 mars 2023, 10 heures 30, TBA

**Giulio Manzonetto** *CANCELLED*

Séminaire des doctorants

Jeudi 23 mars 2023, 16 heures, 3052 and Zoom link

**Robin Vacus** *Introduction to Game-Theory: Braess-like paradoxes*

Automates

Vendredi 24 mars 2023, 14 heures, Salle 3052

**Quentin Manière** *Counting queries in ontology-based data access*

Graph Transformation Theory and Applications

Vendredi 24 mars 2023, 15 heures, online

**Elvira Pino And Fernando Orejas** (Department of Computer Science, Universitat Politècnica de Catalunya, Spain) *A Logical Approach to Graph Databases*

While relational databases were designed upon logical and algebraic foundations, the development of graph databases has been quite ad-hoc. In this sense, the aim of this paper is to provide them with some logical foundations. More precisely, in previous work we introduced a navigational logic, called GNL (Graph Navigational Logic) that allows us to describe graph navigational properties, and which is equipped with a deductive tableau method that we proved to be sound and complete.

In this presentation we will introduce a new formal model for property graphs. Then, we will show how graph queries à la Cypher can be expressed using a fragment of GNL, defining for them a logical and an operational semantics, based on the inference rules for GNL. Finally, we show that both semantics are equivalent.

Vérification

Lundi 27 mars 2023, 11 heures, 1007 and Zoom link

**Lénaïg Cornanguer & Christine Largouët** (IRISA Rennes) *TAG: Learning Timed Automata from Logs*

We consider real-time systems, which can be modeled with Timed Automata: our approach is thus a Timed Automata learner. There is a handful of related work, however, they might require a lot of parameters or produce Timed Automata that either are undeterministic or lack precision. In contrast, we propose an approach, called TAG, that requires only one parameter and learns, without any a-priori knowledge, a deterministic Timed Automaton having a good tradeoff between accuracy and automata complexity. This allows getting an interpretable and accurate global model of the considered real-time system. Experiments compare our approach to related work and demonstrate its merits.

Algorithmes et structures discrètes

Mardi 28 mars 2023, 15 heures, 3052

**Lélia Blin** (LIP6) *Self-Stabilizing Distributed Algorithms*

One world numeration seminar

Mardi 28 mars 2023, 14 heures, Online

**Roland Zweimüller** (Universität Wien) *Variations on a theme of Doeblin*

(Part of this is joint work with Max Auer.)

Preuves, programmes et tout ça

Mardi 28 mars 2023, 13 heures 30, salle 3052

**Fabio Massaioli (Scuola Normale Di Pisa)** (Scuola Normale di Pisa) *A non-trivial proof-semantics for classical sequent calculus (LK)*

Working within the propositional fragment of the context-sharing formulation of LK — where parallel logical rules permute freely — we show that the graph constructed by tracing the history of atomic formula occurrences through axiom and cut rules is invariant under arbitrary rule permutations in cut-free proofs, thus providing a canonical representation of normal-form proofs.

We then introduce a refinement of the notion of axiom-induced graph that allows extending the invariance result to proofs with cuts, although at the cost of a strong assumption on the shape of derivations. Because cut-reduction in this formulation of LK can be implemented entirely by logical rule permutations plus a pair of local rewriting steps that preserve the refined axiom graphs, the result yields a non-trivial invariant of cut-reduction.

Algorithmique distribuée et graphes

Mercredi 29 mars 2023, 14 heures, 3052

**Valentin Bartier** (LIRIS) *Independent set reconfiguration in sparse graphs*