18.nov, 14:00 ICT-315 "Runners in action"
Tarkvarateaduse instituudi seminaril esmaspäeval, 18.11.2019 kell 14:00 esineb Danel Ahman (Ljubljana Ülikool, Sloveenia) teemal "Runners in action".
Seminar toimub ruumis ICT-315.
Runners in action
Runners of algebraic effects, also known as comodels, provide a mathematical model of resource management. We show that they also give rise to a programming concept that models top-level external resources, as well as allows programmers to modularly define their own intermediate "virtual machines". We capture the core ideas of programming with runners in an equational calculus λ-coop, which we equip with a sound and coherent denotational semantics that guarantees the linear use of resources and execution of finalisation code.
We demonstrate runners in action through a variety of examples: hiding file handles from user code while guaranteeing their proper finalisation (by closing them); nesting runners to model user code inside a sandbox inside a VM inside an OS etc; nesting runners to instrument user code with cost models; nesting runners to implement (dynamically monitored and enforced) monotonic state on top of a runner that implements ordinary (non-monotonic) ML-style state; and pairing runners to combine different effects (e.g., state and file IO).
We also accompany λ-coop both with a prototype language implementation in OCaml and a library in Haskell.
This is joint work with Andrej Bauer.