TBA
In this talk we shall discuss the notion of hyperlattices, that is preorders somewhat similar to lattices, but where instead of binary supremums and infimums we consider sets of minimal elements of upper bounds and maximal elements of lower bounds. We will utilize this notion to study superpowersets, that is families of functions defined on nonempty sets with values in hyperlattices, and superpowergroups, that is algebras defined on superpowersets with group-like properties. Numerous examples of such objects appear in topology, logic and algebra, and, in particular, in the algebraic theory of quadratic forms. Finally, we shall distinguish one class of superpowergroups that we call relational superpowergroups, and will see how the category of relational superpowergroups is almost a topos — that is, it satifsies all the axioms of a topos except the subobject classifier axiom. This is joint work with Hugo Mariano and Kaique Matias de Andrade Roberto.
In 1992, Andrew Blass published "A game semantics for linear logic", the first attempt to give meaning to proofs in linear logic in terms of winning strategies for a game. However, the composition of his construction was not associative, the two possible ways to compose three strategies were not necessary equal. Most of the subsequent works saw the non-associativity as an issue that needed to be corrected. In this talk, after explaining the Blass games in details, I will embrace their non-associativity, reveal their actual structure by using Munch-Maccagnoni's duploids, a non-associative model of effects, and show what it tells us about games.
What do the usual set operations (intersection, union, complement,…) and the structure of first-order formulas have in common? In this talk, we will see how both can be described in the context of category theory through the notion of “Doctrines”. After a brief review of first-order logic, we will compare two worlds: we will observe that the set of all subsets of a given set and the set of all first-order formulas that depend on some fixed free variables can be endowed with the structure of a Boolean algebra. This will allow us to show that the powerset functor and indexed families of first-order formulas are both examples of first-order Boolean doctrines. These are categorical structures where logical connectives and quantifiers are interpreted as algebraic operations and adjunctions. Finally, I will give a hint about my current research topic, where I am exploring the concept of “quantifier-free formula” in the doctrinal setting.
Many recent works have studied how analogue models work, compared to classical digital ones. By “analogue” models of computation, we mean computing over continuous quantities, while “digital” models work on discrete structures. It led to a broader use of Ordinary Differential Equation (ODE) in computability theory. From this point of view, the field of implicit complexity has also been widely studied and developed. We show here, using arguments from computable analysis, that we can algebraically and implicitly characterise PTIME and PSPACE for functions over the reals using ODEs.
Within the study of the semantics of programming languages, computational effects may be modelled with monads, and weak distributive laws between monads are then a tool to combine two such effects. The first part of the talk will be dedicated to introducing (monotone) (weak) distributive laws.
In both the category of sets and the category of compact Hausdorff spaces, there is a monotone weak distributive law that combines two layers of non-determinism. Noticing the similarity between these two laws, we study in the second part of the talk whether the latter can be obtained automatically as some sort of lifting of the former.
More specifically, we show how a framework for constructing monotone weak distributive laws in regular categories lifts to categories of algebras, giving a full characterization for the existence of monotone weak distributive laws therein. We then exhibit such a law, combining probabilities and non-determinism, in compact Hausdorff spaces; but we also show how such laws do not exist in a lot of other cases.
The rational base number system, introduced by Akiyama, Frougny and Sakarovitch in 2008, is a generalization of the classical integer base number system. Within this framework two interesting families of infinite words emerge, called minimal and maximal words. We conjecture that every minimal and maximal word is normal over an appropriate subalphabet. To support this conjecture, I will present the results of several numerical experiments that examine the richness threshold and the deviation from uniformity of these words. I will also discuss the implications that the validity of this conjecture would have for several long-standing open problem, such as the non-existence of the so-called Z-numbers and the "Collatz-inspired" 4/3-problem.
This is an expository talk introducing the first concepts of combinatorial category theory. The goal is to present the so-called co-Yoneda lemma, stating that any presheaf is canonically a colimit of representables. We will explain these terms and try to convey some intuition as to why and how the result holds. From my last talk, only categories and functors are expected to be remembered.
In this talk, we will look at some efficient algorithms to recover a message from a corrupted encoding of it. This is a phenomenon that happens all around us, from a phone call to scanning QR codes. We will consider encodings based on low-degree polynomials. We will start with some basic definitions in error-correcting codes, and then we will see few technical lemmas that is useful in designing our algorithms. If time permits, we will also see a cool application of these algorithms for hardness amplification in complexity theory. The talk is aimed at general math/CS audience.
Les circuits algébriques sont un modèle de calcul de polynômes multivariés. Les roABP (read-once oblivious algebraic branching programs) forment également un modèle de calcul pour de tels polynômes. On s'intéresse à une classe particulière : la classe des polynômes calculables facilement par des roABP. Nous pourrions nous demander si cette classe est close par factorisation, c'est-à-dire si tout facteur irréductible d'un polynôme calculable par un petit roABP est également calculable par un petit roABP. Nous étudions également les propriétés de clôture de cette classe spécifique pour d'autres opérations, en comparaison avec d'autres classes de circuits, tels que les formules ou les circuits de profondeur constante.
This talk is an invitation to the algebraic side of category theory. The starting point is the empirical observation that algebraic structures of various sorts are closed under cartesian product. I'll explain how category theory makes this into an abstract result, namely: forgetful functors from monad algebras create binary products.
Constructive foundations have for decades been built upon realizability models for higher-order logic and type theory. However, traditional realizability models have a rather limited notion of computation, which only supports non-termination and avoids many other commonly used effects. Nonetheless, many recent works have shown how realizability models could benefit from side effects to provide computational interpretation for logic principles. In earlier work with Cohen and Tate [1], we addressed the challenge of finding a uniform and generic algebraic framework encompassing (effectful) realizability models, introducing evidenced frames for this purpose. These structures not only enable a factorization of the usual construction of a realizability topos from a tripos—evidenced frames are complete with respect to triposes—but are also flexible enough to accommodate a wide range of effectful models.
We pursued this along two main directions: - first, by extending the syntactic (typed) approach to realizability, following Kreisel’s tradition, where propositions from a ground logic (e.g., HOL) are translated into specifications and typed programs (realizers) that satisfy them. We introduce EffHOL [2], a new framework that expands syntactic realizability. It combines higher-kinded polymorphism—enabling typing of realizers for higher-order propositions—with a computational term language using monads to represent and reason about effectful computations. - second, by generalizing the traditional notion of Partial Combinatory Algebras (PCAs), which underpins classical realizability models. To better internalize a broad spectrum of computational effects, we propose the concept of Monadic Combinatory Algebras (MCAs) [3], in which the combinatory algebra is structured over an underlying computational effect captured by a monad. As we shall see, MCAs provide a smooth generalization of traditional PCA-based realizability semantics.
We consider the problem of reconstructing a graph G from a query Q which, for every k-subset of vertices S, provides some information Q(G)(S) about the induced subgraph G[S]. The vertices are labelled from 1 to n, so reconstruction up to isomorphism is not sufficient, we need to know which label is where. We have studied the case k=3. Given a query Q on triples, we are interested in two things: a structural characterization of all graphs G that are uniquely reconstructible from the function Q(G) (i.e. such that Q(H)=Q(G) if and only if H=G), and a polynomial-delay enumeration algorithm of all graphs that are consistent with some input query answers. In 2023, Qi and Bastide et al. respectively have managed this for the connectivity query (meaning that, for every triple S, Q(G)(S) indicates whether G[S] is connected). We have obtained the same results for all 13 other non-trivial queries on triples. This presentation will go into details of a select few of these queries. Joint work with Hoang La, Raphaëlle Maistre, Matthieu Petiteau and Dimitri Watel.
Ordinals numbers, or transfinite numbers, are a set-theoretic notion allowing to extend the ordered structure of natural numbers beyond infinity. In fact, the collection of ordinals is bigger than any set, and thus contains more elements than we could ever describe with finite sentences.
Still, one can wonder how many ordinals can be expressed with finite sentences. Ordinal notations are systems of syntax that, similar to how one could describe mathematical objects with words, describe with formal terms a given set of ordinals.
In this talk, I will present ordinal notations, an example of their use and describe the notation of Buchholz's psi functions, allowing to define a lot of important countable ordinals.
Synthetic computability can be traced back to Hyland's work on the Effective topos: in this structure, every function is computable, and as such the computability theory can be considered as an internal theory. This also gives an interpretation of oracles for computability as subtoposes of the effective topos. As synthetic computability is based on topos notions, it is also well suited to type theoretic formalism, which will be our framework. In parallel, Homotopy Type Theory (HoTT) emerged to give a type theoretical notion of synthetic homotopy theory. Inside this theory, the notion of space up to path equivalence is primitive (in opposition to set theory, where sets are the primitive notion). A lot of work has been done in recent years to developp this theory, which leads to the work this talk is based on: a paper by Andrew W. Swan describing an adaptation of synthetic computability in HoTT, and the interpretation of oracles as higher modalities. We will see how these notions arise and how they can be generalized to higher types.
Termination is an important property of algorithms, ensuring that they will not run indefinitely. This property is often essential for correctness, yet proving termination can be challenging.
Under the SAPPORO project, we developed an automated technique called Subgraph Counting to prove termination for algorithms modeled as injective double-pushout (DPO) graph rewriting systems. DPO graph rewriting systems model data as graphs and algorithms as sets of rules representing operations that algorithms can perform. Each rule specifies conditions for replacing a subgraph with another.
In this presentation, we focus on the termination of algorithms representable as a single rule. The Subgraph Counting technique relies on the principle that if the number of occurrences of a specific subgraph strictly decreases with each rewriting step, then the rewriting rule will eventually terminates. The key challenge is to estimate the number of occurrences of the subgraph in the graph before and after a rewriting step in an implicit context. We are going to present a sufficient condition on the rewriting rule that makes this estimation possible.
Polynomial diagrams (also known as containers) are a categorification of the notion of polynomial. They can be defined in any category with pullbacks, where they form a bicategory. In the setting of homotopy type theory, we show that the (wild) category of polynomial diagrams in types can be recovered as a Kleisli category over the category of spans of types, thus fitting spans and polynomials respectively as the linear and non-linear part of a homotopical model of Linear Logic. If time allows, I will talk about how this fits in a framework of infinity-categorical models of Linear Logic that we are currently developing.
Proof complexity aims to analyse the power of formal proof systems. Specifically, it is the study of the resources required to certify the truth of mathematical statements. It plays a crucial role in computational complexity and it has close connections to circuit complexity, automated reasoning, and mathematical logic.
A key direction in proof complexity is algebraic proof complexity, which analyses proof systems that use algebraic representations of logical formulas. These systems provide insight into the power and limitations of algebraic methods in proof complexity. Among them, the Ideal Proof System (IPS), introduced by Grochow and Pitassi, is the focus of this talk. IPS represents proofs as algebraic circuits verifying the unsatisfiability of polynomial equations.
In this talk, we will explore the IPS proof system, its connections to algebraic complexity, and recent developments in its study. We will discuss lower bounds for IPS, structural properties of algebraic proofs, and their implications for classical proof complexity questions. Finally, we will highlight open problems and future directions in the field.
Abstract GSOS is a categorical framework for operational semantics, in which rules are modeled as natural transformations of a certain type. Rule systems that fit the constraints imposed by the framework are guaranteed to have desirable properties, mainly that coalgebraic behavioural equivalence, which roughly corresponds to bisimilarity, is a congruence. While bisimilarity is central in process algebra, it is far from the only notion of process equivalence of interest. However, abstract GSOS is not easily applicable to these other equivalences. This work focuses on the other extremum of the linear time-branching time spectrum (bisimilarity being the finest), namely trace equivalence. We wonder under which assumptions on abstract GSOS laws this notion of equivalence is a congruence. A study of trace equivalence for a concrete instance of abstract GSOS (to labelled transition systems with explicit termination) identifies necessary and sufficient conditions to this end. We then transpose abstract GSOS to Kleisli semantics and investigate how, with conditions on the monad (affineness) and the GSOS law (dubbed linearity and smoothness) inspired by the concrete study, trace equivalence can be shown to be a congruence.
Dans cet exposé, je commencerai par mettre en contexte une série de travaux explorant dans un sens large une méthodologie basée sur des représentations «shallow» de calculs dans Rocq. Je me concentrerai ensuite plus spécifiquement sur un travail récent qui argue que de tels interprètes monadiques construits comme des couches d'interprétation empilées sur la monade libre constituent une manière prometteuse d'implémenter et de vérifier des interprètes abstraits.
L'approche permet des preuves modulaires de la correction des interprètes résultants. Nous fournissons des combinateurs génériques de contrôle de flôt abstraits dont la correction est prouvée une fois pour toute relativement à leur contrepartie concrète. Nous démontrons comment relier des gestionnaires concrets implémentant des effets à des variantes abstraites de ces gestionnaires, en capturant essentiellement la correction habituelle des fonctions de transfert dans le contexte des interprètes monadiques. Enfin, nous fournissons des résultats génériques pour transporter les résultats de correction par interprétation des effets d'état et d'échec.
Nous avons formalisé tous les combinateurs et théories susmentionnés dans Rocq, et démontré leurs avantages en implémentant et en prouvant la correction de deux interprètes abstraits illustratifs pour un langage impératif structuré et un assembleur jouet.
Cette contribution est un travail conjoint avec Sébastien Michelland et Laure Gonnord, et a fait l'objet d'un article à ICFP'24.