A verified integration of parallel programming paradigms in CC++

CC++ is an object-oriented parallel programming language that uses parallel composition, atomic functions, and single-assignment variables to express concurrency. We show that this programming paradigm is equivalent to several traditional imperative communication and synchronization models, namely monitors and asynchronous channels. Furthermore, the object-oriented nature of CC++ provides an ideal framework for integrating these paradigms. We specify, implement, and formally verify a collection of libraries that integrates these traditional models with CC++