FP-Syd meeting!

FP Syd June edition features a deep dive into the world of types and modal logic.

Amos Robinson: Fitch-style modal lambda calculi
Modal types give us a way to talk about computations that require restricted contexts, such as embedding pure computations in an impure language. However, previous formalisations of modal types that introduce multiple typing contexts can be unwieldy: they require the introduction of let-expressions for unboxing modalities, and these let-expressions can get in the way of equational reasoning.
In contrast, Fitch-style modal type systems don't require let-expressions and make it easier to perform equational reasoning. Fitch-style modal type systems also offer a semantic interpretation which, I think, makes it easier to understand the real meaning of the typing rules, and how to extend them to different modalities.
In this talk I'll describe a few applications of modal types, and describe the key idea of Fitch-style modal type systems.
(The talk summarises and builds upon Ranald Clouston's 2018 paper)

As usual, doors open at 6pm for mingling and networking. The talk will start at 6:45pm.