A Dependently Typed Parallel Runtime System
As the multi-core CPU architectures are long the standard, writing parallel programs are essential
to extract the maximum performance from the CPU. This project explores the use of dependant
types in creating a model for parallelism, through defining algorithmic skeletons as a dependant type. It describes extending a small, dependently typed programming language pi-forall with a new C++ compilation backend, as well as developing concurrency primitives in the language. Using the primitives, the algorithmic skeletons are defined using dependent types, and furthermore, proofs are created to ensure the correctness of the skeletons.
Keywords
Parallelism, Compilers, Functional Programming, Algorithmic Skeletons
Staff
[Christopher Brown]{cmb21}