Preliminary Programme

9:30-12:00 Workshop on Logic and Computation – 102 (Robert Recorde), Computational Foundry

9:30-9:35 Opening

9:35-10:10 Paulo Oliva (Queen Mary London): On uniform interpretations of quantifiers

10:10-10:20 Coffee Break

10:20-10:50 Arnold Beckmann and Anton Setzer (Swansea University): A Hoare Logic for Access Control

10:50-11:10 Jens Blanck (Swansea University): Domain Theory and Totality

11:10-11:20 Coffee Break

11:20-11:55 Thorsten Altenkirch (University of Nottingham): Uli’s Surprising Hacks

11:55-12:00 Closing

12:00-12:30 Lunch Time

12:30-13:30: EPSRC EPIC International Seminar –  102 (Robert Recorde), Computational Foundry

13:45-15:00: Departmental end of year event – Research Crucible, Computational Foundry

13:45-14:00 Gathering in the Research Crucible for Coffee

14:00-15:00 End of year event

---

Programme Details

Workshop on Logic and Computation	102 (Robert Recorde), Computational Foundry	9:30-12:00
9:30-9:35		Opening
9:35-10:10	Paulo Oliva (Queen Mary University)	On uniform interpretations of quantifiers If we go back to the origins of realizability and the BHK interpretation, quantifications such as \exists x A(x) are interpreted as pairs (a, b) where “a” witnesses x, and “b” witnesses A(a). More recently, however, several realizability interpretations treat quantifiers uniformly:  b realizes \exists x A(x) if \exists x (b realizes A(x))  b realizes \forall x A(x) if \forall x (b realizes A(x)) i.e. b realizes A(x) uniformly (independent of x). Examples of this are Krivine realizability of second-order arithmetic, Ulrich Berger’s realizability of uniform Heyting arithmetic, and van den Berg et. al. Herbrand realizability of internal quantifiers in non-standard analysis. In this talk I’ll discuss current work on identifying the common structure behind such “uniform interpretations of quantifiers”.
10:10-10:20		Coffee Break
10:20-10:50	Arnold Beckmann and Anton Setzer (Swansea University)	A Hoare Logic for Access Control Following Toni Hoare’s seminal invention to reason about computer programs, which is now called Hoare logic, we introduce a related approach to reason about security properties like access control of computer programs. We will define our formalism, state main properties, and explain its connection to weakest preconditions wrt Hoare Logic. We will also present examples to illustrate our point.
10:50-11:10	Jens Blanck (Swansea University)	Domain Theory and Totality Domain Theory is a central concept in various areas of Theoretical Computer Science that was originally motivated from a need in Denotational Semantics to find solutions to domain equations. The resulting spaces have many remarkable properties, including Cartesian closure, and a surprisingly strong connection to computability. A totality has various uses, for example, to lift functions to full domain functions; and for capturing the concept of total information about an element in domain representations. We will give a mostly nontechnical introduction to Domain Theory and give a flavour of some of the results.
11:10-11:2-		Coffee Break
11:25-11:55	Thorsten Altenkirch (University of Nottingham)	Uli’s Surprising Hacks I will present two particularly interesting constructions that Uli has contributed to—both of which I find deeply inspiring. The first, developed jointly with Schwichtenberg, involves inverting the evaluation functional, also known as normalisation by evaluation. Their work sparked my own explorations in this area. The second construction is a remarkable insight from Uli’s PhD thesis: the observation that the ∀ quantifier over boolean streams can be defined for computable functions. This stands out as one of the most surprising and elegant—functional programs I’ve encountered.
11:55-12:00		Closing
EPSRC EPIC International Seminar	102 (Robert Recorde), Computational Foundry	12:30-13:30
12:30-13:30	Deborah Olukan (King’s College London)	The Limits of Detail: Heterogeneity and Parameter Identification in Agent-Based Models Agent-Based Models (ABMs) offer a powerful way to capture heterogeneity in complex systems, particularly in contexts like disease spread and behavioural dynamics. However, increasing agent-level detail comes with a hidden cost: it complicates the calibration process and can lead to parameter identification problems, where multiple parameter combinations produce indistinguishable outcomes. This talk examines how increasing heterogeneity in ABMs, defined here as agent granularity, undermines parameter identifiability and, in turn, affects predictive power. Using a contagion case study and Approximate Bayesian Computation (ABC), we compare homogeneous and heterogeneous model configurations to demonstrate how added complexity can obscure true parameter values. We further explore the real-world consequences of these issues through a hypothetical vaccine hesitancy scenario. The findings highlight the importance of treating calibration and identifiability as interconnected processes and caution against the uncritical use of highly detailed models without assessing their identifiability limits.
Departmental end of year celebration	Research Crucible, Computational Foundry	13:45-15:00
13:45-14:00		Gather in the Research Crucible for Coffee
14:00-15:00		End of year event