In distributed computing, graphs model independent computational units that can communicate only with their neighbors. In this setting, the quality of an algorithm is informally measured either by the amount of exchanged messages, or by the distance the information has to travel during the execution. In this context, simple problems in the centralized setting (such as testing acyclicity or 2-colorability) become hard. However, they become easier if an oracle (knowing the full graph) is allowed to give additional information. For example, a way for the oracle to certify k-colorability consists in giving its color to each node (which may then check that the coloring is proper and uses at most k colors).

The goal of local certification is to minimize the amount of global information needed, while making sure the nodes can collectively test some property even when the oracle is not trustworthy. The sketch above shows that coloration lies among the easiest non-trivial properties to locally certify.

This talk is about presenting the notion of local certification based on joint works with Nicolas Bousquet, Linda Cook, Laurent Feuilloley, and Sébastien Zeitoun. We provide examples of graph properties to illustrate what is easy/hard to certify. We discuss meta-theorems for local certification as well as open problems.

The notion of a local state classifier was introduced in the context of Lawvere’s first open problem in topos theory. Although this problem itself has already been resolved, the idea of local state classifiers—defined as colimits of all monomorphisms—has potential applications in more general categorical frameworks beyond topos theory.

In this talk, I will not delve into the technical details of topos theory. Instead, I will focus on explaining the definition and core idea of the local state classifier through simple examples. At the end of the presentation, I will briefly introduce my research on a topos-theoretic approach to automata theory, which is based on the fact that the local state classifier of the category of word actions PSh(Σ*) is given by word congruences.

Dumont-Thomas numeration systems are a subclass of abstract numeration systems where the factorisation of the fixed point of a substitution is used to represent numbers. A positional numeration system is one where a weight can be assigned to each position so that the evaluation map is an inner product with the weights. For general abstract numeration systems, deciding positionality is an open problem. In this talk, we define an extension of Dumont-Thomas numeration systems to all integers. We then offer a criterion for deciding the positionality of such a system. If time permits, we show a link to Bertrand numeration systems, another familiar class of numeration systems. Joint work with Sébastien Labbé and Manon Stipulanti.

Motivated by the notion of strong computable type for sets in computable analysis, we define the notion of strong computable type for G-shifts, where G is a finitely generated group with decidable word problem. A G-shift has strong computable type if one can compute its language from the complement of its language.

We obtain a characterization of G-shifts with strong computable type in terms of a notion of minimality with respect to properties with a bounded computational complexity. We provide a self-contained direct proof, and also explain how this characterization can be obtained from an existing similar characterization for sets by Amir and Hoyrup, and discuss its connexions with results by Jeandel on closure spaces. We apply this characterization to several classes of shifts that are minimal with respect to specific properties.

This provides a unifying approach that not only generalizes many existing results but also has the potential to yield new findings effortlessly. In contrast to the case of sets, we prove that strong computable type for G-shifts is preserved under products. We conclude by discussing some generalizations and future directions.

This is a joint work with Benjamin Hellouin de Menibus.

Many different kinds of formal systems may be presented as projection functors p : D → C from a more or less complicated category D to some simpler category C, so that natural logical and computational questions about these systems are reduced to lifting problems along the functor. In the talk I will discuss joint work with Paul-André Melliès applying this perspective to automata and formal languages, which leads naturally to a generalization of the theory of regular and context-free languages to languages of arrows in arbitrary categories. Most of the talk will focus on finite-state automata, but time permitting I will also discuss regular and context-free grammars.

Main references by PAM and NZ:

* Functors are type refinement systems, POPL 2015, https://doi.org/10.1145/2676726.2676970 * The categorical contours of the Chomsky-Schützenberger representation theorem, LMCS 21:2, https://doi.org/10.46298/lmcs-21(2:12)2025