Midlands Graduate School in the Foundations of Computing Science

Christmas Seminar, University of Sheffield. Tuesday 17th December 2024.

The MGS Christmas Seminars 2024 will take place on Tuesday 17th December in Lecture Theatre 6 in the Diamond Building at the University of Sheffield.

The Midlands Graduate School (MGS) is an annual spring graduate school on the mathematical foundations of computing science. It has run annually since 1999 and has been held at either the University of Birmingham, the University of Leicester, the University of Nottingham, or at the University of Sheffield. The lectures are aimed at graduate students, typically in their first or second year of study for a PhD, but the school is open to anyone who is interested in learning more about mathematical computing foundations, and all such applicants are warmly welcomed. We very much encourage learners from abroad and from industry to attend, and many have done so in the past. The next 2025 MGS Graduate School will also take place at the University of Sheffield, 7-11 April 2025.

Participation at the Christmas seminar is free to all, and no registration is required.

Programme (Invited Talks)

Social events

Venue

All talks and coffee breaks will take place in the Diamond Bulding in or near Lecture Theater 6, located in the basement. The building is situated on 32 Leavygreave Rd, Broomhall, Sheffield S3 7RD. Due to it being so close to West street, it is easy to get there by bus (lines 51, 52, 95, 95a and 120) and tram (the nearest tram stop being West Street).

Abstracts

Deck the Handlers with Modular Effects. Nicolas Wu, Imperial College London.
Algebraic effects offer a powerful framework for defining and interpreting modular domain-specific languages (DSLs), encapsulating effectful operations within algebraic theories. This talk introduces the `effective` library, a Haskell implementation for modular higher-order effects. The library enables the design of extensible DSLs, recovering modularity for scoped and latent effects while integrating seamlessly with Haskell's monad transformer and I/O systems.

Kleene Iteration: From Kleene Algebra Onwards. Sergey Goncharov, University of Birmingham.
Kozen's celebrated completeness result incepted Kleene algebra (and later Kleene algebra with tests) as a versatile tool for lightweight reasoning about program equivalence. However, numerous variants have since emerged to address the need for more refined semantic frameworks, such as those for stateful, concurrent, exceptional, hybrid, and branching-time systems. From a high-level perspective, the standard notion of Kleene algebra lacks robustness when extended to accommodate specific programming features, as its axioms often conflict with program equivalences in the domain of interest. This raises a fundamental question: what is the most basic axiomatization of Kleene iteration that could serve as a unified, uncontroversial foundation for reasoning about non-deterministic iterative behavior across diverse settings? In this talk, I will discuss recent advances, challenges, and insights in answering this question.

Canonical Labelling of Random Graphs. Maksim Zhukovskii, University of Sheffield.
On an n-vertex input graph, a canonical labelling algorithm computes a bijection from the set of vertices of the graph to {1,..,n} such that, for any other isomorphic graph, their labelled versions (according to the bijection) are identical. Once two graphs are canonically labelled, determining whether they are isomorphic can be done in linear time. The existence of polynomial-time algorithms for testing isomorphism of two given graphs and for producing a canonical labelling remain open. Babai's breakthrough quasi-polynomial algorithm for testing graph isomorphism was subsequently extended to a canonical labelling algorithm of the same time complexity.

Nevertheless, for typical graphs (or, in other words, with high probability for binomial random graphs G(n,p) with p=1/2) it is known that there exists a linear time canonisation algorithm, due to Babai, Erdős, and Selkow (1980). Since then, several results have established efficient canonical labelling algorithms for random graphs across various ranges of edge probability p=p(n). Recently, we filled the last remaining gap and proved that there exists a polynomial-time algorithm that labels canonically the random graph G(n,p) with high probability, whatever the edge probability function p(n). The core of the algorithm is, so called, colour refinement procedure, which distinguishes graphs if and only if they are distinguishable in 2-variable first order logic with counting.

The talk is based on joint work with Oleg Verbitsky.

Organisation

The organisers of MGS 25 are Andrei Popescu (A.Popescu@sheffield.ac.uk) and Georg Struth (G.Struth@sheffield.ac.uk). Please direct all queries about this event to Andrei Popescu.