Rencontre, 26 juin 2025

Programme

10:30 – 12:00

Vikraman Choudhury (Università di Bologna)

Invited talk: The Duality of λ-Abstraction

There are well-known dualities of computation in both functional and concurrent programming: input/output, expression/context, strict/lazy, sender/ receiver, forward/backwards, and several others. When viewed through an algebraic lens, these can be understood as metaphysical interpretations of rigorous mathematical dualities. 

In this talk, I will explore the duality of values and continuations (Filinski'89) through the lens of cartesian closure/co-cartesian co-closure. The main observation is that, just as higher-order functions give exponentials, higher-order continuations give co-exponentials. Using this semantic duality, I will present a λλ~ (lambda-lambda-bar or tilde) calculus, which is a call-by-value calculus extended with a classical disjunction type, that exhibits a duality of abstraction/co-abstraction. I will develop the syntax and semantics of this language, and give a computational interpretation in terms of speculative execution and backtracking. Using the language, I will show how to recover classical control operators, the computational interpretation of classical logic, and axiomatise control effects. Finally, I will show how this duality gives a nice programming idiom for control effects, that can be used in existing functional programming languages.

13:45 – 14:45

Danielle Marshall (University of Glasgow)

Invited talk: Linearity, Uniqueness, Ownership: An Entente Cordiale

Substructural type systems, which restrict the use of weakening and contraction rules from intuitionistic logic, are growing in popularity because they allow for a resourceful interpretation of data which can be used to rule out software bugs. Substructurality is finally taking hold in practical programming: Haskell now has linear types based on Girard's linear logic but integrated via graded function arrows, Clean has uniqueness types ensuring that values have at most a single reference, and Rust has an intricate ownership system guaranteeing memory safety. But despite this broad range of resourceful type systems, there has been comparatively little work on understanding their relative strengths and weaknesses. We demonstrate how linear types and uniqueness types can be used within a single system in the setting of the Granule language to offer both restrictions on local program behaviour and guarantees about global memory usage. We then extend this framework further, by showing that just like graded type systems as in Granule or Idris build upon linearity, Rust's ownership model builds upon uniqueness. We develop an extended type system incorporating ownership and borrowing based on ideas from both fractional permissions and graded types, and implement this in Granule.

15:15 – 16:15

Elaine Pimentel (University College London)

Invited talk: Alternative Semantic Views of Modality: From the Modal Cube to Linear Logic

PART I: A Proof-Theoretic Approach to the Semantics of Classical Linear Logic

Linear logic (LL) is a resource-aware, abstract logic programming language that refines both classical and intuitionistic logic. The semantics of linear logic is typically presented in one of two ways: by associating each formula with the set of all contexts that can be used to prove it (e.g. phase semantics) or by assigning meaning directly to proofs (e.g. coherence spaces).

This work proposes a different approach by adopting a proof-theoretic perspective. More specifically, we employ base-extension semantics (BeS) to characterise proofs through the notion of base support.

PART II: The Modal Cube Revisited: Semantics without Worlds

We present a non-deterministic semantic framework for all modal logics in the modal cube, extending prior works by Kearns and others. Our approach introduces modular and uniform multi-valued non-deterministic matrices (Nmatrices) for each logic. The semantics is grounded in an eight-valued system and provides a sound and complete decision procedure for each modal logic, extending and refining earlier semantics as particular cases. Additionally, we propose a novel model-theoretic perspective that links our framework to relational (Kripke-style) semantics, addressing longstanding conjectures regarding the correspondence between modal axioms and semantic conditions within non-deterministic settings. The result is a philosophically robust and technically modular alternative to standard possible-world semantics.