Research
Notes about my work

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 ualib.org website.
The library is open source and downloadable from the ualib/agda-algebras GitHub repository.