Notes about my work

Reading time: about 10 minutes (2028 words).

NEWS! (2021 Feb 12) The Agda Universal Algebra Library is undergoing a makeover to make it more concise and elegant and to correct some flaws in the previous version. Stay tuned for an announcement of the release of version 2.03 of the Agda UALib, which will appear here in late February 2021.

(2021 Jan 26) The Agda Universal Algebra Library and Birkhoff's Theorem in Dependent Type Theory, documentation for the Agda UALib.

(2021 Jan 20) I am very pleased to announce that on 12 January 2021 I achieved my goal of constructing a formal, machine-checked proof of Birkhoff's variety theorem in dependent type theory using the Agda programming language.

Birkhoff's celebrated theorem asserts that a class K of algebraic structures is closed under the taking of homomorphic images, subalgebras, and arbitrary products if and only if K is defined by a set of equations.

To the best of my knowledge, this is the first time Birkhoff's Theorem has been formulated and proved in dependent type theory and verified with a proof assistant.


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 (43 words).