Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

34

PLDI
1998
ACM

favoriteEmaildiscussreport

96views Programming Languages» more PLDI 1998»

Eliminating Array Bound Checking Through Dependent Types

14 years 3 months ago

Eliminating Array Bound Checking Through Dependent Types

Download www.cs.cmu.edu

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 eﬃciently in practice. We illustrate our approach through concrete examples and present the result of our preliminary experiments which support support the feasibility and eﬀectiveness of our approach.

Hongwei Xi, Frank Pfenning

Real-time Traffic

Array Bound Checking | List Tag Checking | PLDI 1998 | Programming Languages | Type-based Approach |

claim paper

Related Content

» A Dependently Typed Assembly Language

» Subregion Analysis and Bounds Check Elimination for High Level Arrays

» A Fresh Look at Optimizing Array Bound Checking

» Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search

» OnDemand Refinement of Dependent Types

» Static Consistency Checking for Verilog Wire Interconnects

» SAFECode enforcing alias analysis for weakly typed languages

» Typestate Checking of Machine Code

» Asserting Bytecode Safety

Post Info
More Details (n/a)

Added	05 Aug 2010
Updated	05 Aug 2010
Type	Conference
Year	1998
Where	PLDI
Authors	Hongwei Xi, Frank Pfenning

Comments (0)