Submitted for publication.
Arrays over regions of points were introduced in ZPL in the late 1990s and later adopted in Titanium and X10 as a means of simplifying the programming of high-performance software. A region is a set of points, rather than an interval or a product of intervals, and enables a programmer to write a loop that iterates over a region. While convenient, regions do not eliminate the risk of array bounds violations. Until now, languages implementations have resorted to checking array accesses dynamically or to warning the programmer that bounds violations lead to undefined behavior. In this paper we show that a type system for a language with arrays over regions can guarantee that array bounds violations cannot occur. We have developed a core language and a type system, proved type soundness, settled the complexity of the key decision problems, implemented an X10 version which embodies the ideas of our core language, written a type checker for our X10 version, and experimented with a variety of benchmark programs. Our type system uses dependent types and enables safety without dynamic bounds checks.