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.