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

The eighth meeting of the Southern and Midlands Logic Seminar (SMLS) will be held on the afternoon of Wednesday 11th December 2024 at the University of Sussex in Brighton.

Participation in SMLS is free to all, but please contact Giulio Guerrieri if you intend to participate, to help us plan practical arrangements.

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, and by the School of Engineering and Informatics of the University of Sussex.

Programme: Wednesday 11th December, 2024

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 bursaries

Each meeting has a small budget to cover travel costs for speakers and participants. Priority will be given to young researchers, particularly PhD students. We are also able to provide some support for participants with caring or parenting responsibilities. Anyone who requires support should contact Thomas Powell in advance of the meeting.

Abstracts

Unification Modulo Equational Theories in Languages with Binding Operators. Maribel Fernandez, King's College London.
Unification (i.e., solving equations between terms) is a key step in the implementation of logic programming languages and theorem provers, and is also used in type inference algorithms for functional languages and as a mechanism to analyse rewrite-based specifications (e.g., to find critical pairs). Matching is a version of unification in which only one of the terms in the equation can be instantiated. Often, operators satisfy equational axioms such as associativity and commutativity, which should be taken into account during the unification or matching process (cf. Maude).
In addition, when the expressions to be unified involve binding operators (as is the case when representing programs, logics, computation models, etc.), unification and matching algorithms must take into account the alpha-equivalence relation generated by the binders.
In this talk, we will discuss matching and unification algorithms for languages that include binding operators as well as operators that satisfy equational axioms, such as associativity and commutativity.

Zero-one laws: A quantitative insight. Alex Wan, University of Bath.
Zero-one laws are theorems that state that events of a certain type occur with probability 0 or 1. They are fundamental results which have applications in various areas of mathematics, including graph theory. In this talk, I will first reformulate the Borel zero-one law into a computational problem, before stating a specialized result that is linked closely with the Borel-Cantelli lemmas, recently studied by Arthan and Oliva in [1]. I will then take this as a starting point for a more general framework for studying zero-one laws computationally, before demonstrating some applications using this framework, including the zero-one law associated with bond percolation.
Reference: [1] R. Arthan, P. Oliva, On the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone Theorem, Journal of Logic and Analysis 13(6), pp. 1--23, 2021.

Translations between bases in Base-extension Semantics. Yll Buzoku, University College London.
Girard showed that using the exponentials of linear logic, one may embed classical and intuitionistic sequents into linear logic. In particular, such translations give concrete ways of translating intuitionistic sequents into intuitionistic linear sequents.
Since the introduction of a sound and complete semantics Base-extension Semantics (BeS) for Intuitionistic Linear Logic (ILL) there has been a natural question about the relationship between bases which support intuitionistic sequents and the bases used to support ILL sequents; namely, can one translate a base used to support an intuitionistic sequent into one that supports a linear sequent? In this talk, I aim to shed some light on these base translations and show that in fact, such translations exist and that these base translations allow us to recover the Girard translations.

The DeMorganization of a locale. Igor Arrieta, University of Birmingham.
In 2009, Caramello proved that each topos has a largest dense subtopos whose internal logic satisfies De Morgan law (also known as the law of the weak excluded middle). This finding implies that every locale has a largest dense extremally disconnected sublocale, referred to as its DeMorganization. However, explicit examples of DeMorganizations for toposes that do not satisfy De Morgan law are generally rather difficult to find. In this talk, after reviewing some of the basics of locale theory, we present a contribution in that direction, with the main result showing that for any metrizable locale (without isolated points), its DeMorganization coincides with its Booleanization.

Processes as Formulas, and Choreographies as Proofs. Matteo Acclavio, University of Sussex.
In this talk, I discuss proof-theoretic methodologies for studying concurrent programs. In particular, I present a new approach inspired by the standard interpretation of logic program execution as proof search.
For this purpose, I recall syntax and semantics of the recursion-free π-calculus, and I introduce the logic PiL, an extension of multiplicative additive linear logic with a non-commutative non-associative connective (to model the prefix-operator), and nominal quantifiers (to model restriction).
Using a straightforward encoding of processes as formulas, I establish a correspondence between the derivability of a formula in a cut-free sequent calculus and the absence of deadlocks in the encoded process, and between choreographies and proofs.
Finally, I show how proof nets for PiL can provide canonical representatives of computation trees and conclude by outlining potential research directions and applications of this approach.
This talk is based on joint works with Giulia Manara and Fabrizio Montesi

SMLS Organisers

Local Organisers