Tenth Meeting of the Southern Logic Seminar, University of Bath

The tenth meeting of the Southern and Midlands Logic Seminar will be held on the afternoon Tuesday 24 June at the University of Bath. Talks will take place in 1 West 2.101 on the main Claverton Down campus.

Participants are encouraged to join the Southern and Midlands 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 1 West 2.101. 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.

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

"Resource management in programming, call-by-push-value, and ordered logic" Guillaume Munch-Maccagnoni, INRIA Nantes
Although linear logic was seen as a source of inspiration for the design of programming languages (promising to reconcile imperative and functional programming to some, no less!), the integration of notions of linearity in programming language theory has been slow. Examples are rarer to come by than meaningful models of effectful computation determined by monads, as are examples that meaningfully mix linearity and effects. We propose a new example (which meaningfully refines linear logic, and meaningfully mixes linearity and effects) whose motivation is to model the notion of resource from the C++ and Rust programming languages. In these languages, a resource is a value abstraction for some state which requires that some clean-up action is correctly performed at a specific moment. These languages show a possible (and in practice widely successful) way to integrate resources with control (e.g. exceptions). Similarly, our model shows how linearity can be combined with control effects such as the exception monad, exhibiting similar features as C++/Rust. The main tool we use is the decomposition of notions of computation into adjunctions provided by call-by-push-value (CBPV). Somehow, this endeavour requires us to refine the notion of linear CBPV model into an ordered (i.e. non-commutative) CBPV.

"Relational semantics: from simple to non-idempotent intersection types and back" Vincent Sommella, University of Sussex
Relational semantics is a simple and well-studied denotational model for the untyped lambda-calculus. It can be presented syntactically as a non-idempotent intersection type system and provides qualitative and quantitative information, such as the characterization of normalizing terms and their execution time (i.e., the number of steps to reach the normal form). We study the relational semantics for the simply typed lambda-calculus extended with the fixpoint combinator; we show that the interpretation of a simply typed term is nothing but the interpretation of the untyped term restricted to the non-idempotent intersection types refining the simple type. Our approach is based on merging a simply typed derivation with a non-idempotent intersection one, which is not trivial since simply typed terms do not enjoy subject expansion and may not be normalizing (because of the fixpoint combinator). We also show that some (but not all) well-known qualitative and quantitative information provided by relational semantics and non-idempotent intersection type derivations for the untyped lambda-calculus lifts to the simply typed lambda-calculus with fixpoint combinator basically for free, thanks to our results.

"Semantical Analysis of Intuitionistic Modal Logics between CK and IK" Ian Shillito, University of Birmingham
The intuitionistic modal logics considered between Constructive K (CK) and Intuitionistic K (IK) differ in their treatment of the possibility (diamond) connective. It was recently rediscovered that some logics between CK and IK also disagree on their diamond-free fragments, with only some remaining conservative over the standard axiomatisation of intuitionistic modal logic with necessity (box) alone. We show that relational Kripke semantics for CK can be extended with frame conditions for all axioms in the standard axiomatisation of IK, as well as other axioms previously studied. This allows us to answer open questions about the (non-)conservativity of such logics over intuitionistic modal logic without diamond. Our results are formalised using the Coq Proof Assistant.

"On the role of connectivity in Linear Logic proofs" Raffaele Di Donna, Paris Cité/Roma Tre
We investigate a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property applies to the correctness graphs of a proof-structure: it states that any such graph is acyclic and that the number of its connected components is exactly one more than the number of nodes bottom or weakening. This is known to be necessary but not sufficient in multiplicative exponential linear logic (MELL) to recover a sequent calculus proof from a proof-structure. A geometric condition on untyped proof-structures allowing us to turn this necessary property into a sufficient one is presented, and we can thus isolate several fragments of MELL for which this property is indeed a correctness criterion.

"Finding New Applications for Algorithms; Computing Normal Cones with Quantifier Elimination" Ali Uncu, University of Bath
Algorithms usually emerge as solutions to particular problems. They are tools that can find new uses. The more general the algorithm is the more uses it finds. In this talk, we will focus on an example of this. In optimization applications, normal cones play an important role. As the dimensions rise in the problems and at cusp points where the partial derivatives fail to exist, the normal cone calculations become harder. We will shift the problem of calculating normal cones for optimization problems with semi-algebraic constraints to solving quantified logical formulae. We will present some algorithms that compute normal cones using quantifier elimination and real satisfiability. This is based on a joint work with Michael Mandlmayr.

Organisers