/ End of Year & Ulrich Berger’s Retirement Celebration

End of Year & Ulrich Berger’s Retirement Celebration

25th June 2025
9:30 am - 3:00 pm
Add to: Google Calendar | Outlook | iCal File

Programme

9:30-12:00 Celebration in honor of Ulrich Berger’s retirement – 102 (Robert Recorde), Computational Foundry

9:30-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-12:00 Thorsten Altenkirch (University of Nottingham): TBA

12:00-12:30: Buffee lunch (location TBA)

12:30-13:30: HCI. Talks TBA –  102 (Robert Recorde), Computational Foundry

13:30-15:00: Departmental end of year celebration – Research Crucible, Computational Foundry

Programme Details

Celebration in honor of Ulrich Berger’s retirement102 (Robert Recorde), Computational Foundry9:30-12:00
9:30-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:20Coffee 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:20Coffee Break
11:20-12:00Thorsten Altenkirch (University of Nottingham)Talk TBA
Buffet LunchRoom TBA12:00-12:30
Human Computer Interaction (HCI) Talks102 (Robert Recorde), Computational Foundry12:30-13:30
Talks TBA
Departmental end of year celebrationResearch Crucible, Computational Foundry13:30-15:00