Welcome IRIF is a research laboratory of CNRS and Université Paris Cité, also hosting one Inria project-team. The research conducted at IRIF is based on the study and understanding of the foundations of all computer science, in order to provide innovative solutions to the current and future challenges of digital sciences. IRIF hosts about 200 people. Seven of its members have been distinguished by the European Research Council (ERC), six are members of the Institut Universitaire de France IUF), two are members of the Academia Europæa, and one is member of Académie des sciences. Notion of the day Social Networks Follow us on Twitter/X, LinkedIn and Mastodon for our latest news: News 28.11.2024 The Ackermann Award recognizes outstanding dissertations for Logic in Computer Science at ACSL conference. This year, the prize has been awarded to two thesis supervised at IRIF: the laureates are Gaëtan Douéneau-Tabot supervised by Olivier Carton and Emmanuel Filiot at Université Paris-Cité (France) and Aliaume Lopez supervised by Jean Goubault-Larrecq and Sylvain Schmitz at ENS Paris-Saclay and Université Paris-Cité (France), respectively. They will receive their prize to CSL 2025, in Amsterdam, which will take place from 10 to 14 February 2025. 26.11.2024 Congratulations to our following members whose papers have been accepted for the 2025 POPL conference : Rida Ait El Manssour, Guillaume Baudart, Adrienne Lancelot, Giulio Manzonetto, Gabriel Scherer and Mahsa Shirmohammadi 12.11.2024 The LVP (Languages and Program Verification) working group of the GPL GdR of the CNRS will be holding its one-day conference on Thursday 14 November 2024 at IRIF, from 9am to 5.40pm. Emilio Jesús Gallego Aria, Inria researcher at IRIF, University of Paris, will be giving a talk on : ‘Flèche: Incremental Validation for Hybrid Formal Documents’. This event is free but registration is required. 24.10.2024 Does Computer Science Have a Future? That is the question to be debated during the third conference, “We Turn Off, We Reflect, We Discuss,” organized at Université Paris Cité by François Laroussinie. José Halloy (LIED) and Anne-Laure Ligozat (LISN) are the invited speakers. It will take place on December 10, 2024, from 4:15 PM to 6:30 PM. This event is free of charge. 24.10.2024 The Innovation Prize has been awarded to Sergio Rajsbaum, associate member of IRIF, in recognition of his significant contribution to Distributed Computing. The prize will be presented to him at the SIROCCO'25 conference in Delphi, Greece. 31.10.2024 IRIF is excited to host Dexter Kozen from Cornell University as a speaker in our Distinguished Talks series. The talk will take place on December 03, 2024, starting at 11a.m. More details to come! 18.10.2024 We welcome Mélissa Goddé, the new administrative assistant, who has joined the administrative team. 5.11.2024 This year, three IRIF researchers are part of two projects that have won a 2025 Synergy Grant from the European Research Council (ERC). Many congratulations to Valérie Berthé, Hugo Herbelin and Paul-André Melliès ! IRIF wishes them successful results. edit all the past news (These news are displayed using a randomized-priority ranking.) Agenda Enumerative and analytic combinatorics Thursday December 5, 2024, 11AM, IHP Séminaire Flajolet À L'Ihp Bram Petri, Eleanor Archer, Frédéric Chapoton https://semflajolet.math.cnrs.fr/ Non-permanent members' seminar Thursday December 5, 2024, 4PM, Salle 3052 Carmen Arana (PhD Student) How graph theorists use topology In 1955 Kneser conjectured that the k sized subsets of the numbers from 1 to n can be partitioned into n-2k+2 classes such that each class contains only disjoint elements, but that it cannot be partitioned this way into n-2k+1 classes. This conjecture can be nicely expressed as a graph coloring problem. Twenty years later, in order to solve this problem, Lovasz introduced the topological method in graph theory, and more largely combinatorics. In this talk, we will explain what this method entails, and explain how it is used on the example of this theorem. Higher categories, polygraphs and homotopy Friday December 6, 2024, 10AM, Salle 3052 Léonard Guetta Théories homotopiques et modèles algébriques : un cadre général Depuis la célèbre hypothèse d'homotopie formulée par Grothendieck, un thème central de la théorie de l'homotopie et de l'algèbre supérieure consiste à décrire les théories homotopiques d'objets géométriques et topologiques à l'aide de modèles algébriques. Parmi les correspondances fondamentales entre géométrie/topologie d'un côté et algèbre de l'autre, on peut citer : Types d'homotopie ↔ oo-groupoïdes Spectres ↔ oo-groupoïdes symétriques monoïdaux Catégories topologiques ↔ (oo,1)-catégories n-cobordismes ↔ Objets dans une (oo,n)-catégorie monoïdale avec duaux libres sur un objet n-champs localement constants sur un espace X ↔ Représentations du (pro)-n-groupoïde fondamental de X Mais qu'entend-on exactement par “modèle algébrique” ? Suivant le point de vue adopté pour répondre à cette question, le statut des correspondances énoncées oscille entre conjectures et théorèmes. Dans cet exposé, je proposerai un cadre général – la théorie des canevas – qui permet de formaliser précisément cette notion de “modèle algébrique” et de revisiter certaines de ces correspondances sous un angle unifié. Ce cadre nous offrira l'occasion d'aborder des thématiques variées, telles que la théorie des catégories tests, la transition des opérades simpliciales vers les oo-opérades, ou encore les divers résultats de rigidification des structures supérieures. Si le temps le permet, je présenterai également un vaste programme de conjectures et de questions naturelles émanant de ce cadre, ainsi que certains de mes travaux qui s'inscrivent dans cette perspective. Habilitation defences Friday December 6, 2024, 1PM, Salle 2011 (Sophie Germain) Sam Van Gool (IRIF) Logical reflections: Profinite monoids, propositional quantifiers, and temporal operators My HDR manuscript surveys some of the research in algebra, topology, logic, and the foundations of computer science that I have contributed to since completing my PhD in 2014, and suggests directions for further research in this field. The work I report on falls into three research themes: (1) profinite monoids and their relationship to automata and regular languages; (2) uniform interpolation and its relationship to model-complete theories; (3) axiomatization and unifiability for temporal logics. A thematic coherence between these topics lies in the recurring appearance of techniques from infinite model theory and universal algebra for studying finitary phenomena, and the use of projective limits of finite structures. This report aims to show how these techniques help with solving problems in all three of these, a priori different, research themes. The defense will be followed by drinks at IRIF, on the 4th floor of the same building. The manuscript is available via: https://www.samvangool.net/hdr.html Graph Transformation Theory and Applications Friday December 6, 2024, 3PM, online Vincenzo Ciancia (Institute of Information Science and Technologies, National Research Council of Italy) The Topological Approach to Spatial Model Checking This presentation provides an outlook on the topological approach to spatial and spatio-temporal model checking. We introduce spatial logics, the SLCS language, and its semantics applied to various classes of models: Closure Spaces, Graphs, Polyhedra, and Posets. Additionally, we briefly discuss minimization techniques via the Hennessy-Milner property, and current implementation methods, highlighting relevant tools and applications. Special attention is given to how these techniques are used in practical domains such as imaging and 3D mesh analysis. Zoom meeting registration link YouTube live stream Algorithms and complexity Tuesday December 10, 2024, 11AM, Salle 3052 Orr Paradise (UC Berkeley) Models that prove their own correctness This talk introduces Self-Proving models, a new class of models that formally prove the correctness of their outputs via an Interactive Proof system. After reviewing some related literature, I will formally define Self-Proving models and their per-input (worst-case) guarantees. I will then present algorithms for learning these models and explain how the complexity of the proof system affects the complexity of the learning algorithms. Finally, I will show experiments where Self-Proving models are trained to compute the Greatest Common Divisor of two integers, and to prove the correctness of their results to a simple verifier. Joint work with Noga Amit, Shafi Goldwasser, and Guy N. Rothblum. Proofs, programs and systems Thursday December 12, 2024, 10:30AM, Salle 3052 & online (Zoom link) Loïc Pujet (University of Stockholm) To be announced. Syntax Meets Semantics Thursday December 12, 2024, 1:30PM, Salle 3052 Pablo Barenbaum (UNQ, Argentine) A MELL calculus based on contraposition Contraposition is the classical reasoning principle stating that A → B is equivalent to ¬B → ¬A. In typical presentations of classical Linear Logic, e.g. those based on sequent calculus or proof nets, contraposition has no significant computational content, as it corresponds basically to a change of notation. However, for systems in natural deduction style, contraposition exchanges the role of an assumption and a conclusion, which requires to perform a global transformation on the proof. We propose a term calculus for MELL in which contraposition is realized by an operator we dub contrasubstitution, which turns a proof “inside out” to exchange the roles of the conclusion and a specific assumption. We study the properties of this calculus, starting by confluence and strong-normalization. We identify an intuitionistic fragment and show that it simulates various existing classical calculi (such as Parigot's lambda-mu) via Danos et al.'s Q and T translations. Automata Friday December 13, 2024, 2PM, Salle 3052 Vincent Michielini (University of Warsaw) Complexity of Maslov's Class K-bar Maslov’s class K-bar is a fragment of First-Order Logic consisting of formulae in NNF whose variables occurring in the different atoms obey a certain pattern [*]. It embeds many well-known fragments, such as the two-variable fragment, the Gödel fragment (∀∀∃*), some extensions of modal logic… The satisfiability problem for K-bar (does a given formula admit a model?) was shown to be decidable by Maslov in the 60's. Yet its exact complexity has not been established so far, although we know that it is NExpTime-hard (as it captures FO2). In the talk, we complete the picture by showing the following result: every satisfiable formula in K-bar of size n admits a finite model of size at most 2^{O(n log n)}, and therefore the problem is NExpTime-complete. Our approach involves a use of satisfiability games tailored to K-bar and a novel application of paradoxical tournament graphs. This is a joint work with Oskar Fiuk and Dr Hab Emanuel Kieroński, both from Wrocław. [*] the formula phi, written in NNF, is in K-bar if there exists a sequence ∀x1, …., ∀xk of universally quantified variables, not in the scope of any existential one, such that, for every atom of phi, the sequence of its variables either i) admits at most one unique variable, ii) ends with an existential variable, or iii) is exactly the sequence ∀x1, …., ∀xk. Yes, this is complicated. Don't worry, I'll give nice examples. PhD defences Monday December 16, 2024, 10AM, 3052 Avinandan Das (IRIF, CNRS, Universite Paris Cite) Computation with Partial Information : An Algorithmic Investigation of Graph Problems in Distributed Computing and Streaming This thesis discusses the paradigm of computation with partial information, which is necessitated by the infeasibility of processing massive datasets in their entirety. Traditional algorithms, which require full access to input data, become impractical for large-scale problems due to time and space constraints. Several models of computation that allow for partial or incomplete data access, such as property testing, data stream models, distributed computing, and massively parallel computing, have been proposed in the literature. This thesis deals with two models, the distributed LOCAL model and the data stream model in this paradigm. In the LOCAL model, we extend existing frameworks for the well-studied problem of $(\Delta+1)$-proper coloring to a more generalized $k$-partial $(k+1)$-coloring problem, providing novel algorithms and complexity results. Given a $n$-node graph $G=(V,E)$, a $k$-partial $c$-coloring asks for a coloring of the vertices with colors in $\{1,\dots,c\}$, such that every vertex $v\in V$ has at least $\min\{k,\deg(v)\}$ neighbors with a color different from its own color. We extend the rounding based algorithm of Ghaffari and Kuhn (2020), to give a $O(\log n\cdot \log^3k)$ round algorithm and a $O(\log n\cdot \log^2k)$ round algorithm for $k$-partial list coloring and $k$-partial $(k+1)$-coloring respectively. In the data stream model, we introduce the {\em certification} of solutions to computing problems when access to the input is restricted. This topic has received a lot of attention in the distributed computing setting, and we introduce it here in the context of \emph{streaming} algorithms, where the input is too large to be stored in memory. Given a property $P$, a \emph{streaming certification scheme} for $P$ is a \emph{prover-verifier} pair where the prover is a computationally unlimited but non-trustable oracle, and the verifier is a streaming algorithm. For any input, the prover provides the verifier with a \emph{certificate}. The verifier then receives its input as a stream in an adversarial order and must check whether the certificate is indeed a \emph{proof} that the input satisfies $P$. The main complexity measure for a streaming certification scheme is its \emph{space complexity}, defined as the sum of the size of the certificate provided by the oracle, and of the memory space required by the verifier. We give streaming certification schemes for several graph properties, including maximum matching, diameter, degeneracy, and coloring, with space complexity matching the requirement of \emph{semi-streaming}, i.e., with space complexity $O(n\, \mbox{polylog}\, n)$ for $n$-node graphs. For each of these properties, we provide upper and lower bounds on the space complexity of the corresponding certification schemes, many being tight up to logarithmic multiplicative factors. We also show that some graph properties are hard for streaming certification, in the sense that they cannot be certified in semi-streaming, as they require $\Omega(n^2)$-bit certificates. The results presented in this thesis contribute to the growing body of work on algorithms for large datasets, particularly in the contexts of graph theory and distributed systems, and open new avenues for future research in computation with partial information.