29-30 January 2024
Our aim is to bring together a group of researchers interested in the foundations of computer science, but attendance is open for anyone. This website features the programme, some information about the venue, and the abstracts of the talks.
For all inquiries, please contact Andreas Feldmann, Georg Struth or Maksim Zhukhovskii.
Programme
Monday 29.01.
| 10:00 – 10:30 | Coffee | |
| 10:30 – 10:40 | Welcome | |
| 10:40 – 11:30 | Mutual Exclusion: Possibilities and Impossibilities | Rob van Glabbeek (University of Edinburgh) |
| 11:30 – 12:20 | Nominal Recursors as Epi-Recursors | Andrei Popescu (University of Sheffield) |
| 12:20 – 14:00 | Lunch | |
| 14:00 – 14:50 | An Efficient Pseudodeterministic Algorithm for Generating Primes | Rahul Santhanam (University of Oxford) |
| 14:50 – 15:40 | Alice and Bob Walked into a Graph… | Sagnik Mukhopadhyay (University of Sheffield) |
| 15:40 – 16:10 | Coffee | |
| 16:10 – 17:00 | Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach | Harsh Beohar (University of Sheffield) |
| 17:00 – 17:50 | Termination of Higher-Order Probabilistic Programs | Charles Grellois (University of Sheffield) |
| 18:00 – 19:00 | Pub | (optional) |
| 19:00 – | Dinner at Maveli |
Tuesday 30.01.
| 9:00 – 9:50 | Craig Interpolants without Craig Interpolation | Frank Wolter (University of Liverpool) |
| 9:50 – 10:40 | Logics and Complexity Theory on Reals with Connections to Neural Networks | Jonni Virtema (University of Sheffield) |
| 10:40 – 11:10 | Coffee | |
| 11:10 – 12:00 | Moser-Tardos Algorithm with Small Number of Random Bits | Oleg Pikhurko (University of Warwick) |
| 12:00 – 13:40 | Lunch | |
| 13:40 – 14:30 | A Strongly Polynomial Algorithm for the Minimum-Cost Generalized Flow Problem | László Végh (London School of Economics) |
| 14:30 – 15:20 | Parameterized Approximation Schemes for Clustering with General Norm Objectives | Joachim Spoerhase (University of Sheffield) |
| 15:20 – 15:50 | Coffee | |
| 15:50 – 16:40 | Probabilistic Methods for Combinatorial Structures in Isabelle/HOL | Chelsea Edmonds (University of Sheffield) |
Venue
This workshop is hosted by the Foundations of Computation group at Sheffield. It will take place in Lecture Theatre 2 of the Broad Lane Block (BROAD LT2). The venue is easily accessible from the train station by foot or tram in less than 20min. The lecture theatre and reception can be found by the following instructions:
1. Arriving before 10:30 on Monday: there will be coffee served in the Heart Space on floor E, which can be accessed through the entrance on Portobello (see map). When you enter the Heart Space, walk all the way to the back, past the cafeteria and the engineering lab. Behind, you’ll find an elevator that takes you to level E, where coffee is served on the terrace looking down into the Heart Space.
2. If you arrive later than 10:30 on Monday you want to go to the lecture theatre LT2 (room 108) in the Broad Lane block (see map). The easiest path is to enter through the main entrance on Mappin Street (see map), then climbing the stairs one floor to floor E, and turning to the left, following the outer edge of the building. Keep an eye out for the signs labelled Broad Lane Building and then Lecture Theatre 1-5, which will lead you to LT2.
Here are some lunch options:
More information for visitors of the University of Sheffield, including a campus map, can be found here.
Abstracts of Talks
Mutual Exclusion: Possibilities and Impossibilities Rob van Glabbeek (University of Edinburgh)
I will show that under certain assumptions (speed independence and atomicity) no correct mutual exclusion protocol is possible. I also show how mutual exclusion can be achieved when dropping some of these assumptions.
Nominal Recursors as Epi-Recursors Andrei Popescu (University of Sheffield)
Recursors are mechanisms for defining functions by taking advantage of certain structure and properties of the source domains, which often consist of syntactic entities. For example, the denotational semantics of a programming language is specified recursively over the syntax, using a structural recursor. The presence of variable bindings, which are non-local aspects of syntax for programming languages and logical systems, complicates the meta-theory of recursors. Nominal recursors have been specifically designed to cope with binders. They arose within the context of Gabbay and Pitts’s Nominal Logic and related formalisms.
I will revisit nominal recursors from the literature on syntax with bindings and compare them with respect to expressiveness. I will show how nominal recursors can be viewed as epi-recursors, a concept that captures abstractly the distinction between the constructors on which one actually recurses, and other operators and properties that further underpin recursion. I will present an abstract framework for comparing epi-recursors and instantiate it to the existing nominal recursors, and also to several recursors obtained from them by cross-pollination. The resulting expressiveness hierarchies depend on how strictly we perform this comparison, and bring insight into the relative merits of different axiomatizations of syntax.
Finally, I will apply the same methodology to produce an expressiveness hierarchy of nominal corecursors, which are principles for defining functions targeting infinitary non-well-founded terms (which underlie lambda-calculus semantics concepts such as Böhm trees).
An Efficient Pseudodeterministic Algorithm for Generating Primes Rahul Santhanam (Oxford University)
One of the fundamental tasks in computational number theory is to
efficiently generate a prime of length n, given n in unary. The best known
deterministic algorithm (due to Odlyzko and Lagarias) runs in time O(2^{n/2}),
and it is a long-standing open problem to do better.
Gat and Goldwasser initiated the study of “pseudodeterministic” algorithms,
which are randomised algorithms for search problems that output a fixed
solution to the search problem with high probability. They asked if there is a
polynomial-time pseudo-deterministic algorithm for generating primes. I will
describe a line of works culminating in such an algorithm, with the caveat that
the polynomial-time algorithm is only known to work for infinitely many values
of n.
Based on joint work with Lijie Chen, Zhenjian Lu, Igor Carboni Oliveira and
Hanlin Ren.
Alice and Bob Walked into a Graph… Sagnik Mukhopadhyay (University of Sheffield)
I will talk about simple algorithms for cut and flow problems in the 2-party communication setting that can be adapted to many other distributed models of computation quickly. In the realm of data explosion, it is usually the case that a single computational processor is unable to store the vast amount of data needed to do any meaningful computation. We are indeed in the era of distributed computing, but it is not ideal to have different ad-hoc ‘model-dependent’ algorithms for solving the same problem. I will show recent progress in designing cross-paradigm algorithms that tackle this issue.
I will show two examples: the minimum-cut problem (or min-cut) and the maximum bipartite matching problem (or BMM) where, in each case, a simple schematic algorithm can be implemented in several computational models to achieve the optimal complexity. This is a culmination of a number of papers that appeared in the last couple of years with coauthors Joakim Blikstad, Jan van den Brand, Yuval Efron, Troy Lee, Simon Apers, Pawel Gawrychowski, Michal Dory, Andrés López-Martínez and Danupon Nanongkai.
Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach Harsh Beohar (University of Sheffield)
I will present a framework that helps in deriving fixpoint equations from modal logics characterizing behavioural conformances, like behavioural equivalences (bisimilarity, trace equivalences) and their quantitative cousins modelled as metrics. In doing so, we obtain Hennessy-Milner theorems as corollaries to a fixpoint preservation property along Galois connections between suitable lattices. We instantiate this to the setting of coalgebras, in which we spell out the compatibility property ensuring that we can derive a behaviour function whose greatest fixpoint coincides with the logical conformance.
Joint work with Barbara König, Sebastian Gurke, Karla Messing, Lutz Schröder, Jonas Forster, and Paul Wild.
Termination of higher-order probabilistic programs Charles Grellois (University of Sheffield)
I will gently introduce some basics about lambda-calculus, which is the theoretical foundation of functional programming languages, and then explain how to enrich it to allow probabilistic computations. I will also explain the notion of type, and show how we can use them to provide a criterion ensuring that typable probabilistic functional programs terminate almost surely (that is, with probability 1).
Craig Interpolants without Craig Interpolation Frank Wolter (University of Liverpool)
Craig interpolants – logical formulas explaining an entailment between two statements in their shared language – nowadays play a fundamental role not only in mathematical logic but also in applied areas ranging from automated deduction to program verification, databases and knowledge representation. They are used, for instance, as explainers of why sets of program states are disjoint and as synthesisers of concepts, programs and queries.
In this talk, I start with a brief introduction to the Craig interpolation property (CIP) of propositional and first-order logic. CIP states that an interpolant between two formulas exists whenever one entails the other. While propositional and first-order logic enjoy CIP, many important computational logics don’t; examples are finite variable fragments and the guarded fragment of FO, linear temporal logic LTL, decidable hybrid logics, and first-order modal and temporal logics. We consider the interpolant existence problem for such logics (given two formulas, does an interpolant exist) and show that in many cases (but not always) this problem is exactly one exponential harder than entailment. We also discuss the construction of interpolants in these cases.
Logics and Complexity Theory on Reals with Connections to Neural Networks
Jonni Virtema (University of Sheffield)
Descriptive complexity theory is a branch of complexity theory where one uses formal logics to characterise complexity classes. It was shown by Fagin in 1974 that a property of finite structures is decidable in NP if and only if the property is definable in existential second-order logic. The goal of this talk is to survey some adaptations of Fagin-style theorems in the setting of numerical data, and how this approach has recently been useful in charactering the training complexity of neural networks.
In order to generalise Fagin’s theorem to the numerical setting one needs three generalisations: 1) Metafinite structures by Grädel and Gurevich (1998) adds an infinite numerical sort and weight functions to finite structure, 2) Blum-Shub-Smale machines (1989) generalise Turing machines by allowing direct computations with real numbers, 3) logics on metafinite structures utilise the numerical components therein. I will briefly mention the first Fagin-style theorem in this setting by Grädel and Meer (1995) that characterises NP on BSS-machines with a generalisation of existential second-order logic on R-structures (i.e. on metafinite structures where the numerical sort is the reals).
Interestingly, on Boolean inputs, NP on BSS-machines coincides with the complexity class ExistsR (closure of the existential theory of the reals with polynomial time reductions) that has in recent years seen increasing interest. I will conclude by showing that by using a logical approach, we can pinpoint the complexity of training neural networks with diverse activation functions (AAAI 2024). In particular, I will show that the training complexity with the sigmoid activation function coincides with existential theory of the reals with the exponentiation function, whose decidability is an open problem posed by Tarski in the 1950s.
Moser-Tardos Algorithm with Small Number of Random Bits Oleg Pikhurko (University of Warwick)
We present a variant of the parallel Moser-Tardos Algorithm and show that, for a class of problems whose dependency graphs have some subexponential growth, the expected number of random bits used by the algorithm is constant. In particular the expected number of used random bits is independent from the total number of variables. This is achieved by using the same random bits to resample variables which are far enough in the dependency graph.
Joint work with E.Csoka, L.Grabowski, A.Mathe and K.Tyros.
A Strongly Polynomial Algorithm for the Minimum-Cost Generalized Flow Problem László Végh (London School of Economics)
We give a strongly polynomial algorithm for minimum cost generalized flow, and as a consequence, for all linear programs with at most two non-zero entries per row, or at most two non-zero entries per column. While strongly polynomial algorithms for the primal and dual feasibility problems have been known for a long time, various combinatorial approaches used for those problems did not seem to carry over to the minimum-cost variant.
Our approach is to show that the “subspace layered least square” interior point method, an earlier joint work with Allamigeon, Dadush, Loho and Natura requires only a strongly polynomial number of iterations for minimum cost generalized flow. We achieve this by bounding the straight line complexity, introduced in the same paper. The talk will give an overview of the interior point method as well as the combinatorial straight-line complexity analysis for the particular setting. This is joint work with Daniel Dadush, Zhuan Khye Koh, Bento Natura, and Neil Olver.
Parameterized Approximation Schemes for Clustering with General Norm Objectives Joachim Spoerhase (University of Sheffield)
We consider the well-studied algorithmic regime of designing a (1+epsilon)-approximation algorithm for a k-clustering problem that runs in time f(k,epsilon)poly(n) (sometimes called an efficient parameterized approximation scheme or EPAS for short). Notable previous results of this kind include EPASes in the high-dimensional Euclidean setting for k-center as well as k-median, and k-means. However, existing EPASes handle only basic objectives (such as k-center, k-median, and k-means) and are tailored to the specific objective and metric space.
Our main contribution is a clean, simple, and unified algorithm that yields an EPAS for a large variety of clustering objectives (for example, k-means, k-center, k-median, priority k-center, l-centrum, ordered k-median, socially fair k-median aka robust k-median, or more generally monotone norm k-clustering) and metric spaces (for example, continuous high-dimensional Euclidean spaces, metrics of bounded doubling dimension, bounded treewidth metrics, and planar metrics), and which is (almost) entirely oblivious to the underlying objective and metric space.
Key to our approach is a new concept that we call bounded epsilon-scatter dimension — an intrinsic complexity measure of a metric space that is a relaxation of the standard notion of bounded doubling dimension.
This is joint work with Fateme Abbasi, Sandip Banerjee, Jarosław Byrka, Parinya Chalermsook, Ameet Gadekar, Kamyar Khodamoradi, Dániel Marx, and Roohani Sharma. It appears at FOCS’23.
Probabilistic Methods for Combinatorial Structures in Isabelle/HOL Chelsea Edmonds (University of Sheffield)
Formalised libraries of combinatorial mathematics have rapidly expanded over the last five years, but few use one of the most important tools: probability. How can often intuitive probabilistic arguments on the existence of combinatorial structures, such as hypergraphs, be translated into a formal text? I’ll present a modular framework in Isabelle/HOL using locales to formalise such probabilistic proofs, including the basic existence method and first formalisation of the Lovász local lemma, a fundamental result in probability. The formalisation focuses on general, reusable formal probabilistic lemmas for combinatorial structures, rather than a single important theorem, aiming to highlight the potential of modularity and extensibility in modern mathematical formalisations. The applicability of the techniques is demonstrated through the formalisation of several classic lemmas on the existence of hypergraphs with certain colourings. The presentation will conclude with a discussion on some of the fascinating gaps in typical intuitive probabilistic reasoning on paper which were uncovered through the formalisation process, as well as an issue in Isabelle’s current probability libraries.
Foundation of Computation @ Sheffield (FOX) 