WJD Open Notebook

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.

In this post we collect some notes on our experience debugging a faulty touchpad on Hyeyoung's Lenovo X1 (deepersea), which we suspect is a hardware issue. Here are the steps we took to prove this conjecture before we ship the machine to Lenovo for repair.

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.