Seminars & Events
Here at the Swansea University, we host a weekly seminar where we have talks from leading figures in the area of Theoretical Computer Science.
Upcoming
Troy Astarte: Languages, Machines, Expressions: Towards an understanding of the discourse of semantics
The speaker for this week’s seminar is our own Troy. Please find the abstract below. In this talk, I continue to develop my research programme Illustrative Devices of Computing which investigates the historical roots, and educational impacts, of the explanatory and discursive tools used in computing communication. After a brief motivation and review of approaches to the analysis of non-literality, I show my first attempts towards building a taxonomy of IDs using my previous work on the history of programming language semantics for the source. This talk will be a rehearsal for a presentation at the History and Philosophy of......
Archive
Martin Brain: The Pyramid of Formal Software Verification
This week, we’ll have a second theory seminar! Martin Brain from the University of London will come to Swansea to talk about Formal Software Verification. There are a wide range of different approaches to the formal verification of software. They are based on different mathematics, expressed in different terminology and have different ideas of what are important and difficult problems. This makes it hard to compare and contrast different tools. In this talk I will present the pyramid model of formal software verification. It is the result of a decade of working with industrial users and gives a way of......
Kevin Buzzard: Formalizing Fermat
In this week’s theory seminar, we will host a talk by Kevin Buzzard. Abstract I am currently involved in a project to teach a computer proof assistant a proof of Fermat’s Last Theorem. In this talk I’ll explain what a computer proof assistant is, and I’ll try and explain something about the nature of the task, how I ended up doing it, and why I think it’s interesting and important. The talk will be suitable for both computer scientists and mathematicians, and you don’t need any specialized knowledge in computer proof assistants, AI or number theory to follow it. ...
Emmanuel Rauzy: Residual properties of groups in the continuous Weihrauch lattice
In this weeks Theory Seminar, Emmanuel, from the Université de Cétreil, will present his work on ‘Residual properties of groups in the continuous Weihrauch lattice. For every class C of groups, one can define a sort of projection onto C: indeed, every group has a greatest residually C quotient, where a group is residually C if every non-identity element in this group has a non-identity image via a morphism to a group in C. I study how discontinuous this projection map is, in terms of continuous Weihrauch reducibility over the topology of the space of marked groups. This provides a......
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......
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......
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......
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......
Ian Price: 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. ...
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......
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......
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,......
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......
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......
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. ...
An introduction to effective fractal dimension by Benjamin Koch
Today’s theory seminar will be given by Benjamin Koch, who will give as an introduction to effective fractal dimension. Abstract: The purpose of this talk is to give an overview of effective fractal dimension, which is an application of computability theory to geometric measure theory. I will start with an overview of two of the most important notions of dimension in classical measure theory, the Hausdorff and packing dimensions. Following this will be the formulation of so-called effective dimensions for points in R^n via Kolmogorov complexity. The highlight of the study of effective dimension thus far has been the “point-to-set......
Theory Seminar Series
The theory seminar tomorrow will be given by Eike on “Robust Decidability of Escape Problems for General Non-Linear Systems.” Abstract: A wide range of problems from a diverse range of areas can be formulated as “escape problems”: does a given point escape a set under the iteration of a function, or do all points in a given set escape the set under the function. The decidability of these problems is almost exclusively studied under the assumption that points, functions, and sets are specified exactly by a finite amount of data (e.g. rational or algebraic parameters). In this setting, positive results......
Talk on Assuring non-functional requirements
This summer & autumn, our department is hosting Prof Magne Haveraaen (University Bergen, Norway) As part of his involvement in ∆QSD group, he is organising a seminar talk: “Assuring non-functional requirements” Presented by Neil Davies (Bristol) and Peter Thompson (Predictable Network Solutions) Friday, 4. 11, 14:00 CoFo 401 Abstract. Great progress has been made in assuring the functional correctness of digital systems. Coverage analysis, property-based testing, mock environments and formal proof systems can be applied to give very high levels of confidence of correct system behaviour. (That they are all too often not applied is a problem in social science,......
Research visit
Thomas Powell and Davide Barbarossa (Bath University) are visiting Swansea this week. This afternoon Thomas will give a talk on the “Rates of convergence for stochastic processes” as a part of our seminar series. Abstract: I will present two ongoing projects in the new area of proof mining in stochastic optimization, each representing a distinct inroad into the area. First, I will give an account of recent work with Morenikeji Neri that focuses on convergence proofs based on martingales: This quantitative study of martingale convergence has resulted in several variants of the famous Robbins-Siegmund theorem that come equipped with numerical......
Máté Szabó's talk
Máté Szabó is visiting Swansea. He will give a talk today as a part of our theory seminar series: Gödel’s and Post’s Proofs of the Incompleteness TheoremThis talk examines and compares two strikingly different proofs of the first incompleteness theorem. The first proof of the theorem was famously published by Kurt Gödel in 1931. However, during the previous decade, Emil Post already made significant breakthroughs in this topic, even though he was unable to publish his work for various reasons. After taking a short look at Gödel’s diagonal proof, we will engage in more detail with Post’s lesser-known proof. The......
Pieter Collins visiting
Pieter Collins is currently visiting us from Maastricht. Today he will give a talk on “Verified Verification: Formal Proofs of Rigorous Numerical Methods for Model-Checking Dynamic Systems” as a part of our Theory Seminar series. ...
David Trotta visiting Swansea
We are thrilled to extend a warm welcome to Davide Trotta, a postdoctoral researcher at the Department of Computer Science at the University of Pisa in Italy. Davide brings his knowledge and expertise to our community, and we are excited to have him as a guest speaker in our upcoming seminar series, which will take place on Monday, 4 December in our Theory Lab. Title: Categorifying computable reducibilities Abstract: One of the most relevant notions of categorical logic which enabled the study of logic from a purely algebraic perspective is the notion of a (hyper)doctrine, introduced in a series of......
Giovanni Solda visiting Swansea
Next week Giovanni Solda is visiting us from Ghent. He will give a talk on “A combinatorial principle weak over weak systems yet strong over strong systems”. Abstract: Better quasi orders (henceforth bqos) are a strengthening of the notion of well quasi order. Even if their definition is more complicated, the former enjoy nice closure properties that make them, in a way, easier to work with than the latter: this feature made bqos an instrumental tool in proving landmark results like Nash-Williams’ theorem and Laver’s theorem. From the reverse mathematical point of view, the study of bqos is an interesting......