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.
Dr Conor McBride runs the Mathematically Structured Programming group at the University of Strathclyde. He specialises in dependently typed programming. Over a decade ago, he was co-designer and implementer of Epigram. These days, while working on foundational innovations beyond advanced languages like Agda and Idris, he also engages keenly with the languages functional programmers use for real work today. He is one of the people helping to drive the evolution of Haskell's type system towards ever greater expressivity.