Girard's Geometry of Interaction (GOI) can be made concrete by considering it as an implementation technique for functional programs, in particular the lambda calculus. Our work is about the complexity analysis of the abstract machine based on the GOI, the interaction abstract machine (IAM). We have adapted in a non trivial way de Carvalho's non idempotent intersection types so that type derivations completely characterize the time and space complexity of the IAM, thus providing a logical account of the IAM resource usage. Moreover, by the way of the type systems we have introduced, we are able to state some negative results about time and space cost models for the lambda calculus based on the IAM. This is joint work with Beniamino Accattoli and Ugo Dal Lago.

String diagrams are an elegant, convenient and powerful syntax for arrows of symmetric monoidal categories. In recent years, they have been used as compositional descriptions of computational systems from various fields, including quantum foundations, linear algebra, control theory, automata theory, concurrency theory, and even linguistics. All of these applications rely on diagrammatic reasoning, which is to string diagrams as equational reasoning is to ordinary terms.

If we are to take string diagrams out of research papers and into practical applications, we need understand how to implement diagrammatic reasoning. This is the focus of my talk.

There is a tight correspondence between symmetric monoidal categories where every object has a coherent special Frobenius algebra structure and categories of cospans of hypergraphs. This correspondence, therefore, takes us from a topological understanding of string diagrams to a combinatorial data-structure-like description. Moreover, diagrammatic reasoning translates via this correspondence exactly to DPO rewriting with interfaces.

The obvious follow-up question is: how much of this correspondence survives if we drop the assumption about Frobenius structure? Can we use this correspondence to implement diagrammatic reasoning on vanilla symmetric monoidal categories? The answer is yes, but we need to restrict the kinds of cospans we consider: the underlying hypergraph has to be acyclic and satisfy an additional condition called monogamy. Moreover, we must restrict the DPO rewriting mechanism to a variant that we call convex DPO rewriting. The good news is that none of these modifications come with a significant algorithmic cost.

The material in this talk is joint work with Filippo Bonchi, Fabio Gadducci, Aleks Kissinger and Fabio Zanasi, and has been published in a series of papers:

- “Rewriting modulo symmetric monoidal structure”, Proceedings of LiCS 2016

- “Confluence of Graph Rewriting with Interfaces”, Proceedings of ESOP 2017

- “Rewriting with Frobenius”, Proceedings of LiCS 2018

Zoom registration

YouTube live stream

A natural variant of proper vertex colorings, consists in considering colorings which require different colours for vertices at distance (exactly) p, for some fixed p. For that type of colouring, the answer to the question “how many colours suffice?”, can depend greatly on the parity of p. In the talk I will give an overview of the results on this type of colouring, focusing particularly in the case of planar graphs.

We show that for any quantale Q, a Q-category is skeletal and complete if and only if it is injective with respect to fully faithful Q-functors. This is a special case of known theorems due to Hofmann and Stubbe, but we provide a different proof, using the characterisation of the MacNeille completion of a Q-category as its injective envelope.

It is commonly expected that expansions of numbers in multiplicatively independent bases, such as 2 and 10, should have no common structure. However, it seems extraordinarily difficult to confirm this naive heuristic principle in some way or another. In the late 1960s, Furstenberg suggested a series of conjectures, which became famous and aim to capture this heuristic. The work I will discuss in this talk is motivated by one of these conjectures. Despite recent remarkable progress by Shmerkin and Wu, it remains totally out of reach of the current methods. While Furstenberg’s conjectures take place in a dynamical setting, I will use instead the language of automata theory to formulate some related problems that formalize and express in a different way the same general heuristic. I will explain how the latter can be solved thanks to some recent advances in Mahler’s method; a method in transcendental number theory initiated by Mahler at the end of the 1920s. This a joint work with Colin Faverjon.

About the speaker:

Stephen Wolfram is the creator of Mathematica, Wolfram|Alpha and the Wolfram Language; the author of “A New Kind of Science”; the originator of the Wolfram Physics Project; and the founder and CEO of Wolfram Research. Over the course of more than four decades, he has been a pioneer in the development and application of computational thinking—and has been responsible for many discoveries, inventions and innovations in science, technology and business.

Zoom registration

YouTube live stream