4th Southern and Midlands Logic Seminar, University of Birmingham

The fourth meeting of the Southern and Midlands Logic Seminar (SMLS) will be held on the afternoon of Wednesday 13th December at the University of Birmingham. The meeting will take place in room UG09 in the Murray Learning Centre on the main Edgbaston campus.

This event is co-located with the Midlands Graduate School Christmas Seminars 2023, also taking place in Birmingham the next day, Thursday 14th December. Participants of each event are encouraged to attend both! We will organise a social dinner on the evening of Wednesday 13th, between the two events.

Participation is free to all, but please contact Anupam Das if you intend to participate for practical purposes.

Participants are encouraged to join the SMLS community on Slack, which is used for announcements and coordination. Please contact one of the SMLS organisers to be added.

The meeting is supported by a London Mathematical Society Joint Research Groups grant, with additional funding from the UKRI Future Leaders Fellowship Structure vs. Invariants in Proofs (StrIP) and local support from the School of Computer Science at the University of Birmingham.

Programme: Wednesday 13th December, 2023

The programme below is provisional and is subject to change. Last updated 06/12/23.

Venue

The main campus of the University of Birmingham is located in Edgbaston, just outside the city centre. There are frequent trains serving the campus train station (University), about a 10 minute journey from Birmingham New Street. There are also regular buses, but trains will be more convenient for most. Google Maps is reliable for checking train and bus times. It is also possible to travel to/from the campus on foot along the canals, about a 50-60 minute walk from the centre.

All talks, lunch and coffee breaks will take place in UG09 in the Murray Learning Centre on the main Edgbaston campus.

Social events

There will be a social dinner from 18:30, Wednesday 13th December at Hen & Chickens (15 minutes walk from New Street station) between the SMLS meeting and the MGS Christmas Seminars. There will also be a pub social from 18:30, Thursday 14th December at Cherry Reds (5 minutes walk from New Street station) after the MGS Christmas Seminars, where there will also be a festive buffet dinner. If you would like to attend either, please contact Anupam Das as soon as possible, and certainly not later than 24th November.

Before the Christmas Seminars on Thursday 14th many of us will go to the Noble Room for lunch at 12:30. (The Noble Room will be closed for Christmas already!)

Abstracts

Linear Logic-Based Session Types: Expressiveness Results . Nobuko Yoshida, University of Oxford.
The first part of this talk will present an expressiveness result between Linear Logic-based Session Types and System F. The second part gives a summary of recent results on Linear Logic-based Session Types, highlighting the expressiveness correspondence between various session-based process calculi.

The Relational Machine Calculus. Daniel Castle, University of Bath.
The Functional Machine Calculus (FMC) is a generalisation of the λ-calculus capable of effectively reasoning about side effects such as input/output, higher-order mutable store and probabilistic computation. One particularly compelling feature of the FMC is its natural first-order fragment and corresponding string diagram interpretation. By extending this fragment with first-order terms, unification, Kleene star, and nondeterministic sum, we obtain the Relational Machine Calculus (RMC). We show that a variety of models of computation, including interaction nets, Prolog, and Turing machines, may be brought under a unifying framework through natural encodings in the RMC. This new setting allows us to provide operational semantics to graphical formalisms where these may be lacking, while also enjoying close connections to automata.

A Completeness Theorem for Probabilistic Regular Expressions. Wojciech Różowski, University College London.
We introduce Probabilistic Regular Expressions (PRE), a probabilistic analogue of regular expressions denoting probabilistic languages in which every word is assigned a probability of being generated. We present and prove the completeness of an inference system for reasoning about probabilistic language equivalence of PRE based on Salomaa's axiomatisation of Kleene Algebra.

Natural Dualities. Marco Abbadini, University of Birmingham.
In 1936 Stone proved that every Boolean algebra is representable as a subalgebra of the Boolean algebra of subsets of some set. In fact, Stone proved much more, namely that the category of Boolean algebras is dually equivalent to the category of Stone spaces. The beauty of this theorem is that it translates algebraic problems, normally stated in abstract symbolic language, into dual, topological problems, where our geometric intuitions can be brought to bear.

A plethora of similar dualities followed, a prime example being Priestley duality for bounded distributive lattices. In the 80s, these dualities were systematised in the theory of natural dualities. I will give an overview of this theory, which is broad enough to encompass many known dualities, yet concrete enough to generate new ones. Moreover, I will mention an ongoing joint work with Adam Přenosil on extending a portion of this theory to the case in which the so-called dualising object is possibly infinite.

Reflecting on the teaching of theoretical computer science. Achim Jung, University of Birmingham.
Unlike the more applied areas of computing, the canon of theoretical computer science, as far as undergraduate teaching is concerned, seems quite established and stable, comparable to that of mathematics. There are a number of key concepts such as finite automaton, formal language, grammar, Turing machine, and complexity, and some fundamental theorems such as the equivalence between regular expressions, finite automata, and regular languages. In this talk I will look at some of these topics and propose some fundamental changes. A main case study will be the Church-Turing thesis and the pernicious influence it has had on how our discipline is viewed both internally and externally.

SMLS Organisers

Local Organisers