Supervisor

Suitable for

Abstract

Monads serve as a means to encapsulate the impure operations within a computation. They're defined by an adjunction and, in turn, give rise to a specialized form of adjunction known as the Eilenberg-Moore adjunction. Mac Lane's introduction of the comparison theorem [1] provides a framework for connecting these adjunctions unified by a monad through a unique comparison functor. This theorem finds application in certain categorical contexts, as demonstrated by Jacob [2], particularly in interpreting state effects within impure programming languages.

In this project, our objective is to formalize fundamental elements of category theory within the Coq proof assistant. We aim to demonstrate the value of this formalization by certifying Mac Lane's comparison theorem and Beck's monadicity theorems, showcasing the practical utility of our work.

There is an existing formalization of the comparison theorem for the Kleisli constructions in Coq [3], which serves as a promising starting point. Additionally, it is worth noting that the ongoing Coq proof holds strong potential for presentation and publication at conferences such as ITP and CPP, as well as in reputable journals like JFR and JAR.

[1] Saunders Mac Lane. Categories for the Working Mathematician, Graduate Texts in Mathematics, 1978.

[2] Bart Jacobs. A Receipe for State-and-effect triangles, Logical Methods in Computer Science, 2017.

[3] Burak Ekici and Cezary Kaliszyk. Mac Lane’s Comparison Theorem for the Kleisli Construction Formalized in Coq, Mathematics in Computer Science, 2020.

Pre-requisites: a student who wishes to learn Coq is welcome. Familiarity with basic category theory. Familiarity with the Coq proof assistant is also helpful but not required