First Meeting of the Southern Logic Seminar, University of Bath

The inaugural meeting of the Southern Logic Seminar will be held on the afternoon of Thursday 23 February at the University of Bath. Talks will take place in 5 West 2.4 on the main Claverton Down campus.

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

The meeting is supported by a London Mathematical Society Joint Research Groups grant, with additional funding from the Mathematical Foundations of Computation group at Bath.

Programme

Abstracts for the talks are available below.

Venue

The main campus of the University of Bath is located on a hilltop just outside the city centre. It is within walking distance from Bath Spa train station in principle, but you should allow 30–40 minutes and be wary that the route involves a steep uphill climb. A more comfortable alternative is to take one of the regular bus connections from the city centre to the campus. Further information on how to get to the university can be found here, with details of bus routes here.

Talks will take place in 5 West 2.4, which is located in the Department of Pharmacy and Pharmacology. Anyone arriving before lunchtime can find the local participants in the Department of Computer Science, on the fourth floor of 1 West. The campus map might be helpful if you get lost.

Abstracts

"Algebraic structures in relational semantics" Guy McCusker, University of Bath
The well-known relational semantics of linear logic is constructed out of two kinds of free algebra construction: the powerset and the set of finite multisets of a set. This model occupies a central position in denotational semantics. It can interpret typed and untyped lambda-calculus, and is closely related to non-idempotent intersection type systems. In this talk we’ll explore what happens when one varies the algebraic constructions used to build the model. After reviewing some already-known models which arise through the use of different free constructions, we will investigate a new model which is obtained by considering algebras other than the free ones.

"Forcing in type theory" Bruno da Rocha Paiva, University of Birmingham
What was once a set-theoretic concept, forcing is now recognised as a very general tool with applications to many areas of logic. One such application, is for giving models of dependent type theories through presheaf and sheaf categories, where picking the base categories appropriately can yield some level of effects in the resulting type theory. In order to introduce these models, first we look at Kripke semantics, which gives a class of models sound and complete with respect to intuitionistic propositional logic. Then, by relaxing the definition of Kripke semantics, we will get Beth semantics, which are a helpful tool in proving completeness results and can model larger classes of effects. Respectively, these semantics will correspond to a proof-irrelevant version of presheaves and sheaves, paving the way for an introduction of the proof-irrelevant case.

"String diagrams for layered structures" Leo Lobski, University College London
It is customary to think that descriptions of the material reality by different sciences form "layers of abstraction": chemistry is more high-level than physics, biology more high-level than chemistry and so on. We introduce layered props: a diagrammatic framework that is able to handle situations with multiple levels of description, as well as translations between them. To motivate the formalism, we express two examples of scientific modelling as layered props: electrical circuits and retrosynthetic analysis in chemistry. We conclude by showing that the syntactic description of a layered prop can be interpreted naturally as a certain subcategory of pointed profunctors.

"Towards the substitution of proofs" Torie Barrett, University of Bath
In deep inference proof systems, proofs are typically composed by connective and by rule, which are both additive with respect to complexity. We propose a new, multiplicative mechanism for composition, which is given by the explicit substitution of proofs. This compresses proofs, can make normalisation modular, and may lead to a better semantics of proofs.
We have proven some equivalency results for a system with explicit substitutions in the subatomic environment, where logical and structural rules share a single linear rule shape. I will outline these results and some further conjectures, and introduce the techniques that we have developed alongside explicit substitution, including the powerful eversion lemma which may have applications beyond this. I will show how these techniques allow us to transform proofs into systems with a certain notion of very strict linearity with only polynomial complexity cost.

"Deconstructing the calculus of relations with tape diagrams" Alessio Santamaria, University of Sussex
Rig categories with finite biproducts are categories with two monoidal products, where one is a biproduct and the other distributes over it. In this work we present tape diagrams, a sound and complete diagrammatic language for these categories, that can be intuitively thought as string diagrams of string diagrams. We test the effectiveness of our approach against the positive fragment of Tarski's calculus of relations.

Participants

Organisers