This is a project in denotational design, where I am using the proof-gramming language Agda in order to prove certain propositions about parallel algorithms.

I am using techniques from category theory such as closed cartesian categories to model these algorithms in order to make the proofs as elegent as I can.

Currently, I am proving propositions about a parallel tree reduction. Once I am done with that, I will possibly work on parallel mergesort or parallel plus-scan.