ЭФ> список понятий, которые надо знать

1910, теория типов Рассела (Ramified Theory of Types) Уайтхеда и Рассела
1925, простая теория типов Рамсея
1940, простое типизированное лямбда-исчисление Чёрча
1973-1984, конструктивная теория типов Мартина-Лёфа
1988-1992, чистые системы типов Бенарди, Терлоу и Барендрегта (Berardi, Terlouw, Barendregt)

Кто из них умеет в массивы?

Static elimination of array-bounds checking is a long-standing goal for type system designers. In principle, the
necessary mechanisms (based on dependent types—see §30.5) are well understood, but packaging them in a form
that balances expressive power, predictability and tractability of typechecking, and complexity of program annotations
remains a significant challenge. Some recent advances in the area are described by Xi and Pfenning (1998, 1999).