16th Southern and Midlands Logic Seminar, Brighton, University of Sussex

The sixteenth meeting of the Southern and Midlands Logic Seminar (SMLS) will be held on the afternoon of Friday 25th September 2026 at the University of Sussex in Brighton.

Participation in this SMLS meeting is free to all and there is no formal registration, but please contact the local organizer Giulio Guerrieri if you intend to participate, to help us estimate the number of participants and plan practical arrangements such as lunch and coffee breaks. We can refund travel costs for every participant, see below. More information about the venue can be found here.

Participants are encouraged to join the SMLS community on our dedicated mailing list and Discord group, which are used for announcements and coordination. Please contact one of the SMLS organisers or send an email to smls-request@lists.bath.ac.uk to be added to our mailing list and/or Discord group.

The meeting is supported by a London Mathematical Society Joint Research Groups grant, the British Logic Colloquium, and by The Academy of Medical Sciences Networking Grant "Learning from Each Other: Neural Networks and Finite Automata" whose principal investigator is Fredrik Dahlqvist (Queen Mary University London).

Programme: Friday 25th September 2026

After the meeting, we plan to have dinner at 18:30 at the Italian restaurant and pizzeria Fatto a Mano, in the city center, a 7-minute walk from the Brighton train station.


Venue

The meeting will take place in Lecture Theatre 1 at Chichester 1 building (BN1 9QJ), on the campus of the University of Sussex, in Falmer, Brighton and Hove. For a map of the campus, see here.

How the reach the campus of the University of Sussex from Brighton?

Travel refunds

Each meeting has a budget to cover travel costs for all participants: if you attend the meeting, just buy your train tickets, and after the meeting you will receive (very easy) instructions on how to get a refund. We are also able to provide some support for participants with caring or parenting responsibilities; anyone who requires this kind of support should contact Thomas Powell in advance of the meeting.

Abstracts

You Only Get One Shot - Reasoning About One-Shot Undelimited Continuations in Separation Logic. Paulo de Vilhena, University of Surrey.
Continuations are a powerful programming concept: cooperative concurrency, coroutines, Python-style generators, and many other features can be implemented as libraries rather than being built into the language. They usually come in one of two flavours: delimited or undelimited. Although delimited continuations have experienced renewed interest particularly because of the success of effect handlers, undelimited continuations, as offered by call/cc, fell out of fashion because of efficiency concerns and difficulty of reasoning. In this talk, we revisit this old idea of undelimited continuations through the perspective of modern tools such as separation logic. We will see that this exploration indicates an alternative semantics of call/cc that is efficient, enjoys surprisingly simple separation-logic reasoning rules, and can still be used to implement the usual applications of continuations.

Partiality is enriched. Vitek Jelinek, University of Sussex.
Restriction categories are a categorical axiomatisation of partiality: every (potentially) partial morphism comes with a domain of definition, and this domain of definition can be described equationally. In this talk, we will show how restriction categories can be viewed as categories enriched in a certain double category. Cockett and Garner showed that the 2-category of restriction categories is a 2-category of enriched categories. We explain how this can be extended to the whole double category of restriction categories. This is joint work with Nathanael Arkor, Yorgo Chamoun, Bryce Clarke, Hayato Nasu, and Theofilos Tsantilas.

Unbounded Nested Data Automata for Loops in Higher-Order Programs. Adriana Baldacchino, University of Birmingham.
Automata over nested data operate over an infinite alphabet of `data values’, which have an underlying forest structure. Using game-semantic techniques, this hierarchical structure has proved useful in modelling program execution. Previously, these models were limited to bounded depth data, where the underlying tree structure has bounded depth, restricting their application to the study of loop-free programs. We introduce the first model of automata over unboundedly nested data, Unbounded Nested Data Class Memory Automata (UNDCMA). Through UNDCMA, we study contextual reachability and approximation for an ML-like language with loops. Interestingly, emptiness is decidable for UNDCMA, but language inclusion is undecidable. These results imply decidability of reachability, and undecidability of approximation for the language.

A Hilbert method approach to homomorphism equivalence in indexed languages . Richard Mandel, Queen Mary University.
Given a language L \subset \Sigma^* and homomorphisms h,k: \Sigma^* \rightarrow \Sigma^*, the homomorphism equivalence problem (HEP) asks whether h and k are equivalent when restricted to L. We show decidability of the HEP for ET0L languages (a subclass of indexed languages) using a Hilbert method approach, and discuss the obstacles which arise when one attempts to generalize it to the full class of indexed languages.

A fully local proof system for first-order logic. Victoria Barrett, INRIA (France).
In the sequent calculus, the axiom rule can be restricted to propositional or predicate atoms, but this is not possible for the other structural rules such as contraction or cut. By moving to open deduction, a deep-inference formalism in which derivations can be more freely composed and inference rules can apply at any depth inside a formula, we are able to reduce more structural rules to their atomic form. This results in fully local proof systems for propositional classical logic, linear logic, and others in which the inference rules are as small as possible, doing only an amount of work that can be checked in constant time. However, it has been an open question whether the same can be done for first-order logic, where atoms have internal structure due to their term arguments. We show that by extending the syntax and pushing inference rules inside terms, predicates, and quantifiers, we are able to give a fully local proof system for first-order classical logic. We show that this is complete and conservative with respect to the standard system and we anticipate that the small inference rules will lead to good normalisation procedures like they have done in the propositional case.

SMLS Organisers

Local Organisers for the Meeting