By Danel Ahman
On May 21, at 11:00 a.m., in the room FC6 140, Danel Ahman will give a lecture entitled “Temporal resource management via graded effects and graded modal types”.
Title:
Temporal resource management via graded effects and graded modal types
Abstract:
By temporal resources we mean resources occurring in programs whose usage is time-sensitive or -critical, and which, while perhaps already physically available to a program, can be used or acted upon only after a certain amount of time passes or some prescribed events take place (in certain order).
In this talk, I will discuss some ongoing work on using and combining graded effect systems, temporally-aware algebraic effects and effect handlers, and graded modal types for specifying, controlling, and verifying how and when programs use their resources. In particular, I will show how to generalise our past work that only tracked (the lower bounds on) the duration of program execution to a setting where effect grades and resource grades can come from general and not necessarily the same ordered monoids. I will also demonstrate how to extend the underlying calculus with a temporally-aware notion of primitive recursion for covering more realistic and interesting examples.
(This talk is based on past and ongoing joint work with Andres Aluments,
Mariana Milicich, Gašper Žajdela, and Joosep Tavits.)
Bio:
Danel Ahman is an Associate Professor of Programming Languages at the University of Tartu in Estonia. His work focuses on the theory and design of programming languages, with particular interests in algebraic effects and effect handlers, effect systems, dependent and refinement types, modal types, and formally verified software. He received his PhD from the University of Edinburgh, and he has previously held research positions at Inria Paris and University of Ljubljana.