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.