WJD Open Notebook

NEWS! (2021 Mar 7) The long paper on arXiv describing the library is already outdated. However, the complete and always-up-to-date html documentation of the Agda UALib is available on the main ualib.org website.

Pdf documentation will appear in a series of three papers, the first of which is now available as ualib-part1.pdf. Parts 2 and 3 are in the works. Stay tuned.

(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.

A repository containing the files associated with many of my talks can be found at github.com/williamdemeo/Talks.

🔗 2020

• European Online CSP Seminar 2020 - An overview of recent work on bounding the number of homomorphisms into general structures, appearing in our latest paper (arXiv link).

• Völs am Schlern - An overview of some tools for algebra research on 25 Sep 2020.

• Denver - An early version of the UALib documentation used in my talk at the 2020 Joint Mathematics Meetings of the AMS, where I briefly introduced the Agda Universal Algebra Library (UALib).

  • The latest UALib documentation is available from ualib.org.
  • the latest UALib source code is available from gitlab.com/ualib/ualib.gitlab.io.

...there'd be days like these.

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