Type theory should eat category theory for lunch and have monads for breakfast

James Chapman

Institute of Cybernetics

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.

Tarmo Uustalu
Last update 18 November 2009