Join us for a 60 ECTS MSC thesis defence of Calvin Santiago Lee on his thesis Interactions of (co)monads in Agda.

Committee:

• Main supervisor: Tarmo Uustalu, full professor, Reykjavik University, Iceland
• Exequiel Rivas, reseacher, Tallinn University of Technology, Estonia,
• Thorsten Altenkirch, full professor, University of Nottingham, United Kingdom,
• Jana Wagemaker, postdoc, Reykjavik University, Iceland,

Abstract:

We study interaction laws of monads and comonads in a theorem prover. We model effectful computations with monads while comonads model computation-running machines. Interaction laws describe how computations may be uniformly run to yield values. We study monads and comonads on an arbitrary monoidal category, assuming properties such as symmetry only if needed. We do not assume any axioms from classical mathematics which are noncomputable or those which would be incompatible with univalence such as choice, LEM or K. Our formalization is carried out in the Agda theorem prover using the agda-categories mathematical library. It describes interaction laws for functors in general, as well as between monads and comonads. We describe the monoidal category of functor-functor interaction laws. Furthermore, we prove that monoidal objects in the category of functor-functor interaction laws are equivalent to monad-comonad interaction laws. Finally, we develop the end calculus in agda-categories and define the dual endofunctor. We demonstrate several common computationally motivated examples. We show that the monads we consider interact with the expected comonads. We also give examples of the dual. As all formalization is completed in a computable mathematical foundation, this thesis gives a computable theory of computations. This enables future creation of programs which manipulate computations in a verified and general way; for example, compilers or program analyzers.