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.