FP Syd this Wednesday, 25 June
5 views
Skip to first unread message
Jost Berthold
Jun 22, 2025, 9:23:07 PMJun 22
to fp-syd
FP Syd June edition on Wednesday (25th) 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.
Please RSVP on meetup.com or let us know if you intend to join us.
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.
Please RSVP on meetup.com or let us know if you intend to join us.
Reply all
Reply to author
Forward
0 new messages