My main specialty is universal algebra; current projects focus on lattice theory, computational complexity, and universal algebraic approaches to constraint satisfaction problems. Other research interests include logic, category theory, type theory, functional programming, computer-aided mathematical proof and formalization of mathematics.

My **research statement** summarizes some of my research projects. Some of that information can also be found in this post.

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

(Shown above is a general formulation of composition of operations in dependent type theory, as derived here.)

This page is basically a teaser for the lean-ualib package and its detailed documentation (tutorial/textbook) that we are currently developing to formalize important parts of universal algebra in the Lean theorem proving language.

This post collects some notes and teaching materials concerning the use of Python, Jython, and Sage for universal and linear algebra.