Thursday, 19 November 2009, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: In this talk I will describe ongoing work with Thorsten Altenkirch and Tarmo Uustalu to formalise monads and related structures in Agda. I will give some motivation for this work, describe the necessary type theoretic machinery to support our approach, and then go on to describe the subject matter (categories, functors, natural transformations, monads, adjunctions, Kleisli and EM categories etc.) formally in Agda. I will also give some related examples.