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.