Notes about my work

Reading time: about 10 minutes (2039 words).

NEWS! (2021 Nov 30) The unabridged version of our TYPES2021 submission is now available on the arXiv (preprint link). The paper describes our new formal proof of Birkhoff's variety theorem in Martin-Löf type theory using the Agda proof assistant.

More complete documentation of the Agda Universal Algebra Library (agda-algebras) is available on the main website.

The library is open source and downloadable from the ualib/agda-algebras GitHub repository.


Notes about my talks

Reading time: about 3 minutes (709 words).

A repository containing the files associated with many of my talks can be found at

🔗 2020


Notes on my teaching philosophy and experience

Reading time: about 2 minutes (558 words).

My teaching statement discusses my teaching philosophy and experience in great detail. Some of that information can also be found in this post.


posts related to books

Reading time: less than a minute (46 words).