Category Theory and Mechanized Proof

Today I successfully passed my doctorate program’s candidacy examination! You can view the document here. For Drexel’s CS program, our candidacy examination is done during our second year, with the intent of creating a survey of existing work in a fairly narrow area. I selected the intersection of category theory and proof assistants, a research direction which I intend to further explore for the remainder of my PhD.

The paper is technically designed to be somewhat self-contained and briefly reviews some categorical definitions, but in practice is too terse to be considered introductory material. Still, it collects a good deal of information that I have not seen together in exactly this format, so I hope that it can serve as a helpful reference to others with similar interests. Please feel free to reach out if you have any feedback or questions.