Journal of Higher Order and Symbolic Computing manuscript No. (will be inserted by the editor) More Dependent Types for Distributed Arrays

the date of receipt and acceptance should be inserted later Abstract Locality-aware algorithms over distributed arrays can be very difficult to write. Yet such algorithms are becoming more and more important as desktop machines boast more and more processors. This paper shows how a dependently-typed program-ming language can aid in the development of these algorithms and statically ensure that every well-typed program will only ever access local data. Such static guarantees can help catch programming errors early on in the development cycle and maximise the potential speedup that multicore machines offer. At the same time, the functional specification of effects presented here facilitates the testing of and reasoning about algorithms that manipulate distributed arrays.