Patrick Uftring on Computable Transformations of Turing Degree

The speaker for this week's seminar is Patrick Uftring from the University of Munich. He will talk about Computable transformations of Turing degrees. 

Abstract:

Following a conjecture by Vasco Brattka, we present a new result that fully characterizes all partial, multi-valued functions on the Turing degrees that have computable realizers. To be precise, for any such function f mappping n-many Turing degrees to a single Turing degree, there is a subset N of n such that for any degrees a_0, ..., a_n-1, the join of all degrees a_i with i in N is always a solution of f(a_0, ..., a_n-1). This yields short proofs of established results such as [2, Proposition 11.5] but also answers open questions such as "Are two applications of PA reducible to a single instance?" (private communication with Vasco Brattka, cf. [1, Proposition 38]). We also present an infinitary variant, which can e.g. be applied to Weihrauch reductions involving infinite suborders of Turing degrees and answers [1, Conjecture 37]. 

[1] Vasco Brattka, Loops, Inverse Limits and Non-Determinism, arXiv:2501.17734, pp. 1–18. 

[2] Vasco Brattka, Matthew Hendtlass, Alexander P. Kreuzer, On the Uniform Computational Content of Computability Theory, Theory of Computing Systems, vol. 61 (2017), no. 4, pp. 1376–1426. 

CCC 2025 in Swansea

CCC 2025 was an exceptional gathering that perfectly balanced intellectual stimulation with natural beauty. The conference delivered a series of captivating talks that challenged and inspired attendees, while the excursion to Gower provided a refreshing counterpoint to the intense academic discussions. 

Big thanks to our invited speakers, contributors and other participants. See you in Kyoto next year!

CCC in CoFo: Photo by Troy Astarte

CCC in Langland Bay: Photo by Olga Petrovska

 

CCC 2025 Comes to Swansea

This September Swansea will be hosting  CCC 2025 Continuity, Computability, Constructivity - From Logic to Algorithms.

Giovanni Solda on Statistical Learning of Graphs

This Thursday Giovanni Solda will give a talk on statistical learning of graphs as a part of our theory seminar series.

Abstract: In the first part of this talk, I aim to give an introduction to two frameworks that describe when a family of functions can be considered to be learnable, namely PAC and online learnability, and discuss the relationship between them. In the second part, we will apply these frameworks to study the graphs such that the family of their isomorphic copies (with some constraints to be made precise) are learnable. 

This is joint work with Vittorio Cipriani, Valentino Delle Rose, and Luca San Mauro.

Mukesh on Formally Verified Verifiable Group Generators

Mukesh will give a talk on Formally Verified Verifiable Group Generators as a part of our seminar series this Thursday.

Abstract:

Electronic voting (e-voting) requires a trusted setup to initiate an election process. This setup must be transparent to maintain the integrity of the election. A crucial aspect of this trusted setup involves generating group generators for a finite cyclic group, which are then used in cryptographic algorithms deployed within the voting system. Although computing group generators is generally not considered a difficult problem, election verifiability – where every step can be ascertained by independent third parties – excludes many of them, as they fail to provide verifiable evidence of correctness. In this work, we present a formally verified implementation of the group generator algorithm A.2.3 and the group generator verification algorithm A.2.4, specified in the National Institute of Standards and Technology (NIST), FIPS 186-4, in the Coq theorem prover. These two algorithms are highly sought-after methods to compute and verify group generator(s), respectively, because their outcomes can be established independently by third parties. Our formalisation captures all the requirements specified in algorithms A.2.3 and A.2.4 using the expressive type system of the Rocq theorem prover. We evaluate the group generator algorithm within the Rocq theorem prover itself to produce group generators, thereby only trusting the Rocq and its evaluation mechanism. In fact, our implementation is so efficient that it can compute the group generators used in real-world democratic elections in 30 min on a M3 laptop. The source code of this formalisation is available at GitHub [1]. 

[1] https://github.com/mukeshtiwari/Formally_Verified_Verifiable_Group_Generator/ 

Proof and Computation Autumn School

📢 The international autumn school "Proof and Computation" will take place from 14–20 September 2025 in Herrsching near Munich. As a part of it, Ulrich Berger will deliver a course on Program extraction in higher-order logic.

Aimed at PhD students and early-career researchers, the school explores themes across Foundations of Mathematics, Computer Science, and Philosophy, including:

• Predicative Foundations

• Constructive Mathematics & Type Theory

• Computation in Higher Types

• Program Extraction from Proofs

More details and past editions: https://www.mathematik.uni-muenchen.de/~schwicht/pc25.php

Manlio Valenti on the computational strength of a Hausdorff oracle

This Thursday Manlio will give a talk "On the computational strength of a Hausdorff oracle" as a part of our seminar series.

Abstract: Hausdorff dimension is one of the most important notions of dimension in geometric measure theory. It provides a means to describe the "size" of a set in terms of "how tightly" it can be covered with open sets. Recent work has highlighted an interesting connection between the Hausdorff dimension of a set and the computability-theoretical properties of its points. In particular, the effective (Hausdorff) dimension of a point can be defined in terms of its (in)compressibility, so that incompressible (aka random) points have maximum effective dimension. The Point-to-Set Principle states that the Hausdorff dimension of a set can be obtained as the supremum of the effective dimension of its points relative to a fixed parameter (also called oracle). This raises a natural question: how hard is it to compute such an oracle and what is its computational strength? In this talk, we will discuss some recent results in this direction. This is joint work with Ben Koch, Elvira Mayordomo, Arno Pauly, and Cecilia Pradic. 

Davide Trotta's talk

This Thursday Davide Trotta from the University of Padova will give a talk on "A topos for extended Weihrauch degrees" as a part of our seminar series.

Abstract: Weihrauch reducibility [2] is a key notion of reducibility between computational problems that is useful to calibrate the uniform computational strength of a multi-valued function. Such reducibility provides a framework where one can formalize questions such as “which theorems can be transformed continuously or computably into another?”

 The main purpose of this talk is to provide a full categorical account of a generalization of such a notion introduced by A. Bauer called extended Weihrauch reducibility [1]. In particular, we present a tripos [3] and a topos for extended Weihrauch degrees. Then we employ the free constructions and tools developed in [4] to provide a formal connection with realizability, showing that the effective topos is a topos of j-sheaves for a certain Lawvere-Tierney topology over the topos of extended Weihrauch degrees.

This talk is based on joint work with S. Maschio

[1] Bauer, Andrej, Instance reducibility and Weihrauch degrees, Logical Methods in Computer Science 18 (2022), no. 3, 20:1–20:18

[2] Brattka, Vasco and Gherardi, Guido, Weihrauch degrees, omniscience principles and weak computability, The Journal of Symbolic Logic 76 (2011), no. 1, 143–176

[3] Pitts, A. M., Tripos theory in retrospect, Mathematical Structures in Computer Science 10 (2000), no. 3, 283–306

[4] Maietti, M.E. and Trotta, D., A characterization of generalized existential completions, Annals of Pure and Applied Logic 174 (2023), no. 4, Paper No. 103234

 

Weihrauch problems as containers

Today Ian Price will give a talk on "Weihrauch problems as containers" as a part of our seminar series. 

Abstract:

Weihrauch problems can be regarded as containers over the category of projective represented spaces and Weihrauch reductions correspond exactly to container morphisms. Using this characterisation, a number of operators over Weihrauch degrees, including the pomposition of degrees, arise naturally from the theory of polynomial functors.

We are at the 41st British Colloquium for Theoretical Computer Science at Strathclyde University (Glasgow)

BCTCS 2025 at Strathclyde University, Glasgow

Marek Jezinski, Alec Critten, Harry Bryant and Olga Petrovska are currently attending the 41st British Colloquium for Theoretical Computer Science at Strathclyde University, Glasgow.

Marek gave a talk on "Creating Synthetic Test Data for Rail Design Tools", Alec gave a talk on "Developing user propagators for graph-based SMT reasoning", and Harry gave a talk on "Proof Checking for SMT-solving and its application in the Railway Domain."

Olga, who is also BCTCS' Treasurer, will contribute to the education session with her talk on "The Art of Teaching Theory Across Diverse Backgrounds."

On Threshold Problems for Orbits of Semigroup Actions by Eike

Today Eike Neumann will give a talk on Threshold Problems for Orbits of Semigroup Actions as a part of our theory seminar series.

Abstract:

Consider the following computational problem: Given a real function g on a space X, a compactly generated semi-group S acting on X, and a point x in X, is g positive on every point of the orbit of x under S?

This generalises a large number of widely studied problems, such as safety and liveness verification for discrete-time dynamical systems (corresponding to semi-groups with a single generator), threshold problems for stochastic (corresponding stochastic matrices acting on probability distributions) or quantum automata (corresponding to unitary operators acting on Hilbert spaces) and more.

When the objects above are presented via rational or algebraic data, the associated problems quickly become undecidable or very sensitive to the problem formulation. For example, threshold problems for stochastic automata are undecidable in general, and threshold problems for quantum automata are decidable if and only if they are formulated using strict inequality.

I will consider the above problem in its general form from the computable analysis perspective, replacing decidability with maximal partial decidability. I will give a sound algorithm that partially decides the problem over effectively locally compact spaces. I will show that the algorithm is complete when the space is zero-dimensional or locally contractible, and give some examples of spaces where the algorithm is not complete but the problem is maximally partially decidable and spaces where the problem is not maximally partially decidable at all.

Giorgio Genovesi on Characterizing Regular Countable Second Countable Spaces in Second Order Arithmetic

Today's seminar talk is by Giorgio Genovesi from Leeds, who will be talking about countable second countable topological spaces in the context of reverse mathematics. 

Title: Characterizing Regular Countable Second Countable Spaces in Second Order Arithmetic

Abstract: Regular countable second countable (CSC) spaces admit rather nice characterizations and can easily be formalized in second order arithmetic. It is natural to ask what set existence axioms are needed to ensure regular CSC spaces remain nice. It turns out many theorems which characterize regular CSC are equivalent to one of the big five subsystems of second order arithmetic.

Hideki Tsuiki visiting Swansea

Professor Hideki Tsuiki from Kyoto University is visiting Swansea University from 22nd to 24th of January. Yesterday, he gave a talk on Coinductive View of Shadows of 3D Fractals. 

The talk did not only give insight into a fascinating area of research, but was also entertaining. You may want to check out some of Prof. Tsuiki's videos, e.g. https://www.youtube.com/watch?v=VsFD37f-2ck  

Elvira Mayordomo visiting Swansea

Elvira Mayordomo is visiting us this week. Today she gave a talk as a part of our seminar series.

Title: On information theory in geometric measure theory

Abstract

Effective and resource-bounded dimensions were defined by Lutz in 2003 and have proven to be useful and meaningful for quantitative analysis in the contexts of algorithmic randomness, computational complexity and fractal geometry.

The point-to-set principle (PSP) of J. Lutz and N. Lutz (2018) fully characterizes Hausdorff and packing dimensions in terms of effective dimensions in the Euclidean space, enabling effective dimensions to be used to answer open questions about fractal geometry, with already an interesting list of geometric measure theory results.

In this talk I will review the point-to-set principles focusing on recent applications and extensions and presenting open questions as well as further application opportunities.

Theory Away Day

Our Theory Research Group kicked off the year with an inspiring away day, providing the perfect opportunity to reconnect as a team after the festive break. It was a chance to reflect on past successes, align our goals, and spark fresh ideas to drive our work forward in 2025. Here's to an exciting year of collaboration and innovation!

 

Oliver Kullmann's talk

Today Oliver Kullmann will give a talk on Automated search for special Latin squares as a part of our Seminar series.

Abstract: 

Latin squares have been studied since the days of Euler. After some overview on the history and background, an effort for a complete enumeration of special types of Latin squares of order 13, by as completely automated means as possible (which is currently actually not possible), will be presented and evaluated. The main method here is Cube-and-Conquer, a kind of 2-stage SAT-solving (as invented by the presenter). Quite some fine-tuning of representation and choice of solver was needed, and will be discussed (at some high level)

Matteo Acclavio visiting Swansea

Next week's theory seminar will be given by Matteo Acclavio from the University of Sussex, who is visiting us for a few days. The topic will be a new logical framework for concurrent programs, abstract below.

Title: A new logical framework for concurrent programs

Abstract:
Designing logical frameworks to reason about the properties of concurrent programs while accurately capturing the essence of concurrency is a challenging task.
The main difficulties can be traced back to the syntactic constraints of the languages used for this purpose.

In this talk, I will present my ongoing line of research, which aims to provide a new computation-as-deduction paradigm for the study of concurrent programs.
In particular, I will show you a non-commutative logic where we can interpret proofs as computation trees for the pi-calculus, and use proof nets to provide canonical representations of these trees modulo interleaving concurrency.

This work is based on joint works with Giulia Manara and Fabrizio Montesi

Next week's Theory Seminar Series

Next week Troy will give a talk on Conceptualising Programming Language Semantics as a part of our seminar series.

Abstract:

Research on the semantics of programming language has tended towards formalisation. Following the successful deployment and myriad uses of formal syntax, many of those working on semantics assumed similar successes would be realised with formal semantics. 

The reality was different, and the resultant language specifications were large, complicated, technical artefacts. My previous historical research has studied those from a technical perspective. 

In this talk, I will explore the conceptual surroundings of the semantics, examining the use of metaphors, analogies, and illustrative language used to accompany or explain the formal documents.

It is early stage research and will focus primarily on picking examples from the history of semantics for deeper analysis in the future.

I will also present some philosophical frameworks I am considering for use in this analysis and begin to discuss how they might help us understand the topic.

This research will ultimately lead to a conference presentation and journal article next year, as well as forming a pilot study for a research grant proposal.

Galileo Sartor's talk

Today's theory seminar talk will be by Galileo Sartor on "Representing and reasoning with legal aspects of traffic rules for autonomous vehicles". 

Abstract:

In this talk, I will give an overview of a modular system for representing and reasoning with legal aspects of traffic rules for autonomous vehicles.
We focus on a subset of the United Kingdom's Highway Code (HC) related to junctions.
As human drivers and automated vehicles (AVs) will interact on the roads, especially in urban environments, we claim that an accessible, unitary, high-level computational model should exist and be applicable to both users.
Autonomous vehicles introduce a shift in liability that should not bring disadvantages or increased burden on human drivers.
The proposed system is built of three main components: a natural language interface, using Logical English, used to encode the rules; an internal representation of the rules in Prolog; and a simple multi-agent-based simulation environment, built in NetLogo. The three components interact: Logical English is internally translated in Prolog, and the resulting code (along with some support code) interfaces with NetLogo with a bridge.
Such a modular approach enables the different components to carry different ``burdens'' in the overall system; it also allows replacing modules.
With the NetLogo simulation, we can visualize the effect of the modeled rules as well as validate the system with a simple dynamic running scenario.
Designated agents monitor the behaviour of the vehicles for compliance and record potential violations where they occur. The information on potential violations is then utilized by validator agents, to determine whether the violation is punishable, differentiating between exceptions and cases.

Georg Moser visiting

Georg Moser, Prof of Computer Science at University of Innsbruck, is visiting again this week to continue our work on the Royal Society funded project MARRY: MARRYing the analyses of feasible algorithms and problems.