LFCS Seminar: Monday 14 September: Danel Ahman | LFCS

Mon, 14 Sep, 4.10pm

Venue: AT 2.14 (note unusual place and day)

Title: A deeper dive into combining graded monads and graded modal types for temporal resource management

Abstract: In this talk, I will take a deeper dive into the calculus for combining

generally graded monads and generally graded modal types for

specifying, controlling, and verifying temporal properties of

programs' resources which I also talked about at the Plotkin 80

symposium. To recall, by such resources we mean ones whose usage is

time-sensitive and/or time-critical, and which, while perhaps

already physically available to a program, can be used or acted upon

only after a certain amount of time has passed or some prescribed

external events have taken place (perhaps in some order, perhaps not).

In the talk, I will discuss some of the design choices underlying the

calculus, and explore in more depth both its stateful temporally aware

operational semantics and its presheaves-based denotational

semantics, including their relationship. I will also discuss some

extensions to the calculus for modelling more realistic programming

scenarios.

(This talk is based on past and ongoing joint work with Andres Alumets,

Mariana Milicich, Gašper Žajdela, and Joosep Tavits.)

This article was published on Monday 31 August 2026