Eliminating array bound checking through dependent types

We present a type-based approach to eliminating array bound checking and list tag checking by conservatively extending Standard ML with a restricted form of ...