TBA
TBA
TBA
TBA
The goal of this talk is to introduce skeletal semantics, a software framework for specifying and analysing programming languages, and provide a mathematical foundation for it. To this end, we will first introduce SKI calculus as an example of a target programming language and we will show how skeletal semantics can be used to specify it. In a second part, we will motivate our mathematical setting by introducing initial algebra semantics and Lawvere theories, before studying virtual double theories. They are a virtual-double-categorical extension of the latter, allowing for the interpretation of some morphisms as relations. Finally, we show that a skeletal specification (in particular the one of the SKI calculus) may be interpreted as a presentation of a virtual double theory, so that its category of models provides the intended language.
In this seminar, I will focus on bijective digitized rotations in 2D and 3D. In the first part, I will present several new methods to approximate digitized rotations with bijective transformations. These methods, along with several classical approaches, are compared both in terms of accuracy with respect to Euclidean rotations and in terms of computational complexity. In the second part, I will focus on the characterization of bijective digitized rotations in 3D. While this characterization is well known in 2D, its extension to 3D remains an open problem. To address this, I will particularly focus on 3D non-surjective digitized reflections. Finally, some experimental results obtained with DGtal will be presented.
Gallina, the programming language underlying Rocq, has relatively efficient evaluation mechanisms. But sometimes this is not enough: we would like to write some computationally intensive part in a more suitable, off-the-shelve language. I will demo and discuss our current prototype which extends the Rocq kernel to allow declaring and calling native foreign functions. On the user-facing side, it rests on a monad similar to Haskell's IO, featuring unbounded iteration, error, imperative buffers and, well, foreign function calls. To allow reasoning on this monad we provide a weakest precondition program logic defined using Iris. This logic is already flexible enough to axiomatize the specification of most integer functions in GMP[0] and we hope to interface it with existing Rocq semantics for other languages such as C with VST[1] or Capla[2].
[0] https://gmplib.org/
[1] https://vst.cs.princeton.edu/
[2] https://fresco.gitlabpages.inria.fr/capla/language/index.html
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.