Coq formalization of the Habanero programming model.
Brenner is a calculus for reasoning about task parallelism and barrier synchronization. This calculus distils the semantics of phasers and unifies the synchronisation patterns of various abstractions.
Aniceto is a library that helps Coq development. It includes a libray of properties on graph theory.