https://semflajolet.math.cnrs.fr/

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.

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.

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

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

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.

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.

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.

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.