The Theoretical Cosynus Seminar

The theoretical cosynus seminar is aimed at PhD students and young researchers (but older are also welcome) of the Coynus team (but people from other teams are also welcome) in order to have informal presentations about

in the areas of fundamental computer science. This is intended as a safe space to discuss research being done, or share interest about research from others. More mature works are typically presented in the proofs and algorithms seminar.

Everybody is welcome to subscribe to the mailing-list or to the calendar.

Emily Clement (IRIF) – Classification of random groups
05 November 2024 at 14:00 in Marcel-Paul Schützenberger

We study the geometrical properties of random groups, which are group representation G = ⟨S R⟩ where generators S are fixed but where relations R (sentences that cancel subwords of elements of the group) are picked randomly under a density parameter d ∈ [0, 1], with a fixed length. This has been studied before when relations are reduced or cyclically reduced words. In our case we extend these results to relations written as unreduced words, i.e. sentences allowing subwords as gg^{−1} or g^{−1}g, using graph theory. In particular, we prove Triviality property for d ∈ [1/2, 1] and hyperbolicity property for d ∈ [0, 4/9]. The hyperbolicity property is a crucial property, as hyperbolic group, also called automatic groups, can be translated using automata.

Eliot Medioni (LIX) – Complexité locale de la structure dirigée d’un groupe de Lie non commutatif
01 October 2024 at 13:00 in Marcel-Paul Schützenberger

Tout groupe de Lie admet une structure naturelle d’espace localement dirigé. Une stratégie raisonnable pour étudier la structure de cet espace est de le décomposer en ouverts de structure plus simple et de recoller les informations avec un théorème du type Seifert-Van Kampen. Cependant, pour un groupe de Lie non commutatif, aucun ouvert n’a une structure isomorphe à celle d’un ouvert de ℝⁿ, ce qui remet en cause les approches à base de décompositions en sous-espaces.

Manon Blanc (LIX) – Characterisation of PSPACE over the reals: space corresponds to precision
24 June 2024 at 16:00 in Marcel-Paul Schützenberger

It has been proved that (classical) time complexity corresponds to the length of the involved curves, i.e. to the length of the solutions of the corresponding polynomial ODEs. The question of whether there is a simple and robust way to measure space complexity remains. We argue that space complexity corresponds to precision and conversely.

Concretely, we propose and prove an algebraic characterisation of FPSPACE, using continuous ODEs. Recent papers proposed algebraic characterisations of polynomial-time and -space complexity classes over the reals, but with a discrete-time: those algebras rely on discrete ODE schemes. Here, we use classical (continuous) ODEs, with the classic definition of derivation and hence with the more natural context of continuous-time associated with ODEs. We characterise both the case of polynomial space functions over the integers and the reals. A major consequence is that the associated space complexity is provably related to the numerical stability of involved schemas and the associated required precision. We obtain that a problem can be solved in polynomial space if and only if it can be simulated by some numerically stable ODE, using a polynomial precision.

Thea Li (LIX) – Fibrational perspectives on determinization of finite state automata
06 June 2024 at 16:00 in Marcel-Paul Schützenberger

In a recent paper, Mellies and Zeilberger gave a categorical definition of non-deterministic automata as functors with finite fibers and the ULF property. In this talk we will present two determinization procedures for these automata and their respective universal properties, one based on the powerset-monad, which recovers the standard determinization algorithm, and one based on the relative multiset-monad, which is “path-relevant”.

Pierre Loisel (INRIA) – An introduction to code-based cryptography
27 May 2024 at 16:00 in Philippe Flajolet

Public-key cryptography is everywhere: it’s your smartphone, when you pay with your credit card, when you’re updating your software… All of these schemes base their security on the hardness of classical number theory problems: integer factorization (RSA), discrete logarithm over an abelian group (ECDSA)… However, in 1994, Peter Shor published a quantum algorithm which solves all these problems in polynomial time. Even though quantum computers will not be widely used for a (very?) long time, the cryptographic community has to start thinking about quantum-resistant schemes. This has led us to the birth of post-quantum cryptography.

Among all the different approaches to post-quantum cryptography, one of them consist of designing schemes where security relies on the decoding problem of a random linear code. This method, known since 1978, still resists quantum computers. The goal of the talk is to give an introduction to code-based cryptography and, for the sake of illustration, I will present a recent work in collaboration with Thomas Debris-Alazard and Valentin Vasseur about an attack on a code-based signature scheme: enhanced pqsigRM.

Hugo Delavenne (LIX) – Prove your honesty with verifiable computing
15 May 2024 at 16:00 in Philippe Flajolet

Tired of having your friends not trusting you even though they are weaker than you? Tired of being forced to hide things from your partner? The people around you believe that you are faking your life?

The only viable solution to all your problems is verifiable computing! With this revolutionary technique you can generate short proofs that what you claim to do is actually what you are doing, with only a slight increase in your daily complexity, and even dumb people can verify¹ this in a logarithmic complexity. More advanced protocols even allow you not to reveal everything you saw or did while proving a more general claim on this. For instance you could claim not to have been to a bar without revealing your real location (that was hanging out with someone else).

Using the latest error-correcting codes, these protocols are combinatorially safe, without any cryptographic assumption². Only relying on proximity tests and techniques close to compilation, our teams are now able to use in practice the celebrated PCP theorem³. Join us now to have a quadratic discount on your first proofs⁴.

(1) Verifiable computing does not aim to prove that what you are doing is correct, but only to prove that what you are doing is what you claim to be doing. (2) The only cryptographic assumption is the existence of a hash function. (3) The locality of proofs here is logarithmic and not constant. (4) Offer limited to the first 20 provers and only for the two first proofs. See the details on https://delaven.net.

Mehdi Zadem (LIX) – Goal Abstraction in Hierarchical Reinforcement Learning via Reachability Analysis
22 January 2024 at 16:00 in Philippe Flajolet

However, the existing Hierarchical Reinforcement Learning (HRL) approaches relying on symbolic reasoning are often limited as they require a manual goal representation. The challenge in autonomously discovering a symbolic goal representation is that it must preserve critical information, such as the environment dynamics.

I will present a developmental mechanism for subgoal discovery via an emergent representation that abstracts (i.e., groups together) sets of environment states that have similar roles in the task. This mechanism is integrated in a HRL algorithm and shown to be data-efficient, transferrable and interpretable on a set of navigation tasks.

Elies Harington (LIX) – Introduction to Homotopy Type Theory
23 November 2023 at 16:00 in Kateryna Lohvynivna Yushchenko

Homotopy Type Theory (thereafter, HoTT) is a logical foundation for mathematics developed in the early 2010’s. Like the name suggests, the fundamental objects in HoTT are homotopy types, rather than sets. Homotopy types are mathematical objects that first arose in the study of algebraic topology : there a homotopy type is just a topological space up to a “weak homotopy equivalence”. However since then a number of ways of defining homotopy types in set theory have been discovered, so much so that an entire theory has been developed for studying and comparing different models of homotopy types : the theory of Quillen Model Categories. In HoTT however, there is no particular choice of a model : HoTT is the internal language of the theory of homotopy types. Hence every proof in HoTT is automatically true in any particular model.

From the point of view of Computer Science, HoTT is based on Martin Löf’s Type Theory (rather than on first order logic like in the case of ZFC), which makes it very prone to formalization in formal proof assistants. The main axiom distinguishing HoTT from ordinary MLTT also has a nice type-theoretic interpretation : the invariance of properties of data structures under a suitable notion of isomorphism.

In this talk, I will present Homotopy Type Theory, and explain the main ideas and intuitions to have when working in homotopy-theoretic mathematics.

Martin Krejca (LIX) – Evolving Probability Distributions
06 November 2023 at 16:00 in Philippe Flajolet

Heuristic optimization is performed in a multitude of ways. A very common strategy is to create a set of solutions, typically drawn at random, and to then iteratively update it by modifying the solutions randomly, keeping good solutions and eliminating bad ones. An interesting alternative approach is to maintain a probabilistic model instead of a solution set. In this approach, solutions are sampled randomly according to the model, and the model is then updated based on the observed distribution of good samples.

In this talk, we provide a rough overview of the mathematical analysis of algorithms that encompass both of the above approaches, known as randomized search heuristics. We then focus on an algorithm class that follows the second approach, so-called estimation-of-distribution algorithms (EDAs). We discuss the general ideas that go into proving run time guarantees for EDAs and the problems that arise when considering more complex EDAs.

Titouan Carette (LIX) – Graphical Linear Algebra
23 October 2023 at 16:00 in Philippe Flajolet

Linear algebra is everywhere, and anyone studying mathematics, physics, computer science or engineering will have to master some of it at some point. It seems then surprising that the very abstract category theory, particularly string diagrammatic notation, can bring new insights about what is often considered a very basic piece of mathematics. In this talk, I will introduce the linear relation formalism and the associated diagrammatic language. I will go through many elementary notions of linear algebra purely pictorially. The content of this talk is mainly inspired by the work of Fabio Zanasi, Pawel Sobocinski, Filippo Bonchi, and others, with some concepts and notations imported from my work on quantum diagrammatic languages. https://graphicallinearalgebra.net/2015/04/23/makelele-and-linear-algebra/

Émile Oleon (LIX) – Delooping cyclic groups with lens spaces in homotopy type theory
09 October 2023 at 16:00 in Philippe Flajolet

Lens spaces can be described as quotients of the 3-dimensional sphere by (free) actions of cyclic groups. They were first introduced by Tietze in 1908, and have played an important role in the study of manifold topology throughout the 20 century. They were for instance the first known example of 3 dimensional manifolds whose homotopy type is not caracterised by the classicals invariants of algebraic topology (that is homology and homotopy groups).

The construction of such spaces can be generalised in higher dimensions, allowing us to define approximations of the homotopy type of K(ℤₖ,1), the delooping of the cyclic group with k elements. In particular we can construct in that way a model of K(ℤₖ,1) by considering an inductive limit. We will see how to replicate these constructions in the homotopy type theory setting. The interest of such an approach is that the model of Bℤₖ we will obtain is cellular, as opposed to classical models of group deloopings in HoTT (e.g. via the type of G-torsors or via truncation). It thus open the way to a the computation of the cohomology of ℤₖ in homotopy type theory.

Morgan Rogers (LIPN, Paris Nord) – Actegories: the generic setting for monoid acts
19 October 2022 at 16:00 in Philippe Flajolet

The microcosm principle is the informal idea that given an algebraic theory, the most general setting in which such structures can be defined is obtained by lifting the theory to the level of categories. For monoid acts, also known as modules, this results in the notion of actegory, which consists of a monoidal category M (the most general setting in which monoids can be defined), an ordinary category C (the class of objects on which the monoids shall act) and an action of the former on the latter given by a functor C × M → C satisfying some compatibility conditions with respect to the monoidal structure on M. In this talk I’ll explain my motivation for studying these things and give a bunch of examples. Disclaimer: I only came to this topic recently, so I will not be presenting big or novel results; this is just a window into my monoid action adventure.

Bryce Clarke (LIX) – An introduction to enriched cofunctors
06 October 2022 at 16:00 in Philippe Flajolet

Many concepts in category theory may be generalised to the enriched setting where we are able to capture a wider range of examples. The basic notions of category, functor, and natural transformation all admit straightforward generalisations when enriching in an arbitrary monoidal category, and form the basis of enriched category theory. Cofunctors are another kind of morphism between categories which capture a notion of lifting, and the recent introduction of cofunctors between weighted categories by Perrone has motivated the development of an enriched version. This talk has three goals: (1) to introduce the definition of a cofunctor enriched in a distributive monoidal category; (2) examine the duality between enriched functors and cofunctors and state what it means for them to be compatible; (3) discuss several examples of enriched cofunctors for various bases of enrichment, including enrichment in weighted sets. This talk is based on joint work with Matthew Di Meglio (https://arxiv.org/abs/2209.01144).

Samuel Mimram (LIX) – Division by 2, in homotopy type theory
28 September 2022 at 16:00 in Grace Hopper

Natural numbers are isomorphism classes of finite sets and one can look for operations on sets which, after quotienting, allow recovering traditional arithmetic operations. Moreover, from a constructivist perspective, it is interesting to study whether those operations can be performed without resorting to the axiom of choice (the use of classical logic is usually necessary). Following the work of Bernstein, Sierpiński, Doyle and Conway, we study here “division by two” (or, rather, regularity of multiplication by two). We provide here a full formalization of this operation on sets, using the cubical variant of Agda, which is an implementation of the homotopy type theory setting, thus revealing some interesting points in the proof. As a novel contribution, we also show that this construction extends to general types, as opposed to sets. This is joint work with Emile Oleon.

Louis Lemonnier (LMF, University Paris-Saclay) – Central Submonads and Notions of Computation
07 June 2022 at 14:00 in Nicole Reine Lepaute

The notion of “centre” has been introduced for many algebraic structures in mathematics. A notable example is the centre of a monoid which always determines a commutative submonoid. Monads (in category theory) can be seen as generalisations of monoids and in this paper we show how the notion of centre may be extended to strong monads acting on symmetric monoidal categories. We show that the centre of a strong monad T, if it exists, determines a commutative submonad Z of T , such that the Kleisli category of Z is isomorphic to the premonoidal centre (in the sense of Power and Robinson) of the Kleisli category of T. We provide three equivalent conditions which characterise the existence of the centre of T. While not every strong monad admits a centre, we show that every strong monad on well-known naturally occurring categories does admit a centre, thereby showing that this new notion is ubiquitous. We also provide a computational interpretation of our ideas which consists in giving a refinement of Moggi’s monadic metalanguage. The added benefit is that this allows us to immediately establish a large class of contextually equivalent terms for monads that admit a non-trivial centre by simply looking at the richer syntactic structure provided by the refinement.

Bryce Clarke – An introduction to delta lenses
19 May 2022 at 14:00 in Nicole Reine Lepaute

Delta lenses are functors equipped with a suitable choice of lifts, and were first introduced in 2011 to model so-called bidirectional transformations between systems. In this talk, I will provide an introduction to several category-theoretic perspectives of delta lenses which were developed throughout my PhD research. Categories, functors, and delta lenses organise into a double category, and I will demonstrate how many interesting properties of delta lenses may be studied via this two-dimensional categorical structure.

Cameron Calk – Abstract strategies and formal coherence
21 April 2022 at 14:15 in Nicole Reine Lepaute

Kleene algebra have widespread use in mathematics and computer science, from formal language theory to program correctness. Following formalisations of abstract rewriting results in modal Kleene algebra, globular 2-Kleene algebras were introduced, providing a formal setting for reasoning about coherence proofs in abstract rewriting systems. On the other hand, normalisation strategies give a categorical interpretation of the notion of contracting homotopies, constructed via confluent and terminating rewriting. This approach relates standardisation to coherence results in the context of higher dimensional rewriting systems. In this work, we formalise the notion of normalisation strategy in the setting of globular 2-Kleene algebras. In such structures, normalisation strategies allow us to prove a formal coherence theorem via convergent abstract rewriting.

Aly-Bora Ulusoy – A Really Short Hike Through Model Theoretical Galois Theory
29 March 2022 at 14:00 in Nicole Reine Lepaute

Short talk about the Galois theory applied to models of first-order theories. Using symmetry arguments to express non-computability.

Roman Kniazev – Why should study directed loop spaces?
22 March 2022 at 14:00 in Nicole Reine Lepaute

In the first part of the talk, we will discuss classical links of loop spaces with homotopy and (co)homology, together with recognition principle relating loop spaces and operads. In the second part, we will tentatively introduce analogous constructions and suggest possible developments in the context of directed spaces.