thanks for visiting. behind the tabs above are most of my papers, some of the slides from my talks or courses, and on the right are links to the recordings of some recent ones. the publication details for the papers are in this BibTeX base.
a recent paper:
Quotients in monadic programming: Projective algebras are equivalent to coalgebras (with Peter-Michael Seidel)
Abstract. In monadic programming, datatypes are presented as free algebras, generated by data values, and by the algebraic operations and equations capturing some computational effects. These algebras are free in the sense that they satisfy just the equations imposed by their algebraic theory, and remain free of any additional equations. The consequence is that they do not admit quotient types. This is, of course, often inconvenient. Whenever a computation involves data with multiple representatives, and they need to be identified according to some equations that are not satisfied by all data, the monadic programmer has to leave the universe of free algebras, and resort to explicit destructors. We characterize the situation when these destructors are preserved under all operations, and the resulting quotients of free algebras are also their subalgebras. Such quotients are called projective. Although popular in universal algebra, projective algebras did not attract much attention in the monadic setting, where they turn out to have a surprising avatar: for any given monad, a suitable category of projective algebras is equivalent with the category of coalgebras for the comonad induced by any monad resolution. For a monadic programmer, this equivalence provides a convenient way to implement polymorphic quotients as coalgebras. The dual correspondence of injective coalgebras and all algebras leads to a different family of quotient types, which seems to have a different family of applications. Both equivalences also entail several general corollaries concerning monadicity and comonadicity.
a recent course:
Synopsis. What is Computer Science about? What is a computer? What is a recursive function? Why is the Halting Problem undecidable? What is a supercompiler? Answers in pictures.
some old web pages with older stuff which i didn’t transfer:
- at Kestrel Institute (1999-2009)
- at Oxford University (2008-2012)
- Cloudfactory (up to 2006)
- Royal Holloway (2010-2013)