Доброго времени суток!

Я обнаружил на LtU презентацию "The Next Mainstream Programming Languages" (http://www.cs.princeton.edu/~dpw/popl/06/Tim-POPL.ppt).

Среди прочего, там есть идея (думаю, дико бородатая), что можно вводить дополнительные ограничения на данные, что гарантируют попадание всех индексов в массив (как частный случай):

Transform{n:nat}(Vertices:[n]Vertex, Indices:[]nat<n, m:Matrix):[]Vertex=
    for each(i in Indices)
       Transform(m,Vertices[i])

Вроде разумно и хорошо. Но абсолютно непонятно, как это может работать.
В простейшем случае, когда массивы и их значения извесны на этапе компиляции — все более-менее шоколадно. Но что если все это дело загружается, скажем, из внешнего мира и изначально не ясно, выполняются ли эти условия? Видимо тогда надо вручную делать некий if-then-else, что в одной из веток выполнения гарантирует какие-то ограничения. Плюс, должна быть какая-то система доказательств и, желательно, автоматическая система вывода ограничений.

Известно ли уважаемой публике
* что это будет за система типов?
* есть ли готовые примеры реализации?
* что можно почитать на этот счет?