Dimitrios: formalize nominal adapton in Agda
I'd like to learn Agda, which is a proof assistant with interactive
features to facilitate formalizing mathematical statements and constructing
proofs of them. It's also a dependently-typed total functional programming
language. For this project, I'd provide an overview of Agda and explore how it allows users to incrementally develop programs/proofs.
I have a particular application in mind as well, namely in using Agda to verify that certain representations (data types or values) of categories with additional interesting structure, such as free symmetric cartesian categories, satisfy laws of those categories that we want to hold. This will be helpful for a WIP Haskell library that provides users with Monad-like syntax for
Category and various versions of
Formalize \lambda_NomA from the OOPSLA15 paper, with the end goal of proving from-scratch consistency, as described in its appendix.