Keynote: SpaceMonads

Livehacking in Agda, I'll show how space (in this case, rectangular spaces on your screen) has a monadic structure, and build something a little bit like a window-manager before your very eyes (apart from the bits that are behind other windows, which will, of course, remain out of sight). On the way, I'll need to refine some standard testing machinery to produce evidence about what is being tested, and demonstrate that Tony Hoare basically understood monads for dependent types before I was born. The video of this talk will scupper a homework I was thinking of setting my fourth-years, but I don't care.