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.

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

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.

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 information, with applications including stochastic quasi-Fejer monotone sequences and gradient-descent type algorithms. Second, I will report on some work in progress with Nicholas Pischkeon a new stochastic alternating Halpern-Mann scheme with noise terms: In addition to new convergence results (both qualitative and quantitative), this project has led to an interesting application in reinforcement learning, demonstrating that the techniques of proof mining are relevant for current research in the mathematics of artificial intelligence.

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. 

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 area still full of open questions.
In this talk, we will focus on a property of non-bqos, the so-called minimal bad array lemma, and in particular one version of it that we will call MBA − . We will show that MBA − has a very odd behavior when it comes to its reverse-mathematical strength, namely 

• over ATR 0 , MBA − can be seen to be equivalent to the very strong principle of Π 12 -comprehension, yet
• over ACA 0 , MBA − does not imply ATR 0.
In order to prove this result, we will provide a characterization of the quasi-orders that ACA 0 proves to be bqos.

 
This is joint work with Anton Freund, Alberto Marcone, and Fedor Pakhomov.