| Abstract Eliminating Array Bound Checking Through Dependent Types* (2008) | |||||||||||||||
Abstract | |||||||||||||||
| 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 dependent types. This enables the programmer to capture more invariants through types while type-checking remains decidable in the-ory and can still be performed efficiently in practice. We il-lustrate our approach through concrete examples and present the result of our preliminary experiments which support sup-port the feasibility and effectiveness of our approach. 1 | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||