Sciweavers

Share
PLDI
1998
ACM

Eliminating Array Bound Checking Through Dependent Types

10 years 1 months ago
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 dependent types. This enables the programmer to capture more invariants through types while type-checking remains decidable in theory and can still be performed efficiently in practice. We illustrate our approach through concrete examples and present the result of our preliminary experiments which support support the feasibility and effectiveness of our approach.
Hongwei Xi, Frank Pfenning
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where PLDI
Authors Hongwei Xi, Frank Pfenning
Comments (0)
books