Eliminating array bound checking through dependent types
- 1 May 1998
- proceedings article
- Published by Association for Computing Machinery (ACM)
- Vol. 33 (5) , 249-257
- https://doi.org/10.1145/277650.277732
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 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.Keywords
This publication has 9 references indexed in Scilit:
- The design and implementation of a certifying compilerPublished by Association for Computing Machinery (ACM) ,1998
- Proof-carrying codePublished by Association for Computing Machinery (ACM) ,1997
- PVS: Combining specification, proof checking, and model checkingPublished by Springer Nature ,1996
- Optimizing array bound checks using flow analysisACM Letters on Programming Languages and Systems, 1993
- Eliminating false data dependences using the Omega testPublished by Association for Computing Machinery (ACM) ,1992
- Refinement types for MLPublished by Association for Computing Machinery (ACM) ,1991
- Optimization of range checkingPublished by Association for Computing Machinery (ACM) ,1982
- On the SUP-INF Method for Proving Presburger FormulasJournal of the ACM, 1977
- Implementation of an array bound checkerPublished by Association for Computing Machinery (ACM) ,1977