John Nicholson’s Webpage

I am a fourth year PhD student at McMaster University in Hamilton Ontario. My research supervisor is Matt Valeriote. I am interested in the connections between universal algebra and theoretical computer science. My work focuses on applying the tools of universal algebra, namely tame congruence theory, to problems in the theory of regular tree languages. I am also very interested in the formalization of mathematics in LEAN. I am currently involved in a project formalizing multi-sorted model theory in Lean. You can check out the project here.