article

Free access

Eliminating array bound checking through dependent types

Authors:

Frank PfenningAuthors Info & Claims

ACM SIGPLAN Notices, Volume 33, Issue 5

Pages 249 - 257

https://doi.org/10.1145/277652.277732

Published: 01 May 1998 Publication History

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.

References

[1]

Blelloch, G. E. (1993, April). NESL: A nested data-parallel language (version 2.6). Technical Report CMU-CS-93-129, School of Computer Science, Carnegie Mellon University.

Digital Library

[2]

Chow, F. (1983). A portable machine-independent global optimizer- design and measurements. Ph.D. dissertation, Stanford University. Technical Report 83-254.

Digital Library

[3]

Constable, R. L. et al. (1986). Implementing Mathematics with the Nuprl Proof Development System. Englewood Cliffs, New Jersey: Prentice-Hall.

Digital Library

[4]

Corman, T. H., C. E. Leiserson, and R. L. Rivest (1989). Introduction to Algorithms. Cambridge, Massachusetts: The MIT Press.

Digital Library

[5]

Davies, R. (1997, November). Practical refinement-type checking. Thesis Proposal.

Digital Library

[6]

Dowek, G., A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner (1993). The Coq proof assistant user's guide. Rapport Techniques 154, INRIA, Rocquencourt, France. Version 5.8.

[7]

Freeman, T. (1994, March). Refinement Types for ML. Ph.D. dissertation, Carnegie Mellon University. Available as Technical Report CMU-CS-94-110.

Digital Library

[8]

Freeman, T. and F. Pfenning (1991). Refinement types for ML. In A CM SIGPLAN '91 Conference on Programming Language Design and implementation, Toronto, Ontario, pp. 268-277.

Digital Library

[9]

Gupta, R. (1994). Optimizing array bound checks using flow analysis. A CM Letters on Programming Languages and Systems ~(1-4), 135-150.

Digital Library

[10]

Hayashi, S. (1991). Singleton, union and intersection types for program extraction. In A. R. Meyer (Ed.), Proceedings of the International Conference on Theoretical Aspects of Computer Software, pp. 701-730.

Digital Library

[11]

Jay, C. and M. Sekanina (1996). Shape checking of array programs. Technical Report 96.09, University of Technology, Sydney, Australia.

[12]

Markstein, V., C. J. and P. Markstein (1982). Optimization of range checking. In SIGPLAN '8~ Symposium on Compiler Construction, pp. 114-119.

Digital Library

[13]

Martin-LSf, P. (1980). Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science VI, pp. 153-175. North-Holland.

[14]

Michaylov, S. (1992, August). Design and Implementation of Practical Constraint Logic Programming Systems. Ph.D. thesis, Carnegie Mellon University. Available as Technical Report CMU-CS-92-168.

Digital Library

[15]

Necula, G. (1997). Proof-carrying code. In Conference Record of 2$th Annual A CM Symposium on Principles of Programming Languages, pp. 106-119. ACM press.

Digital Library

[16]

Necula, G. and P. Lee (1998, June). The design and implementation of a certifying compiler. In A CM S{GPLA N '98 Conference on Programming Language Design and Implementation. ACM press.

Digital Library

[17]

Owre, S., S. Rajan, J. Rushby, N. Shankar, and M. Srivas (1996, July/August). PVS: Combining specification, proof checking, and model checking. In R. Alur and T. A. Henzinger (Eds.), Computer-Aided Verification, CA V '96, Volume 1102 of LNCS, New Brunswick, N J, pp. 411-414. Springer-Verlag.

Digital Library

[18]

Pugh, W. and D. Wonnacott (1992). Eliminating false data dependences using the Omega test. In A CM SIG- PLAN '9~ Conference on Programming Language Design and Implementation, pp. 140-151. ACM Press.

Digital Library

[19]

Pugh, W. and D. Wonnacott (1994, November). Experience with constraint-based array dependence analysis. Technical Report CS-TR-3371, University of Maryland.

Digital Library

[20]

Shostak, R. E. (1977, October). On the SUP-INF method for proving Presburger formulas. Journal of the A CM 2~ (4), 529-543.

Digital Library

[21]

Sun Microsystems (1995). The Java language specification. Available as ftp://ftp, j avasof t. corn/does/j avaspec, ps. zip.

[22]

Susuld, N. and K. ishihata (1977). Implementation of atray bound checker. In 4th A CM Symposium on Pricipies of Programming Languages, pp. 132-143.

Digital Library

[23]

Xi, H. (1997, November). Some examples of DML programming. Available at ht tp: //www. cs. cmu. edu/~hwxi/DML/examples/.

[24]

Xi, H. (1998). Dependent Types in Practical Programming. Ph.D. thesis, Carnegie Mellon University. Forthcoming.

Digital Library

Cited By

Melquiond GMoreau J(2024)A Safe Low-Level Language for Computer Algebra and Its Formally Verified CompilerProceedings of the ACM on Programming Languages10.1145/36746298:ICFP(121-146)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674629
Economou DKrishnaswami NDunfield J(2023)Focusing on Refinement TypingACM Transactions on Programming Languages and Systems10.1145/3610408Online publication date: 17-Oct-2023
https://dl.acm.org/doi/10.1145/3610408
Hattori MKobayashi NSato R(2023)Gradual Tensor Shape CheckingProgramming Languages and Systems10.1007/978-3-031-30044-8_8(197-224)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_8
Show More Cited By

Index Terms

Eliminating array bound checking through dependent types
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
      2. Language types
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Eliminating array bound checking through dependent types
PLDI '98: Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation

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-...
Dependent types in practical programming
POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index objects are drawn from a constraint domain C, leading to the DML(C) language schema. This allows specification and inference of ...
Practical dependent type checking using twin types
TyDe 2020: Proceedings of the 5th ACM SIGPLAN International Workshop on Type-Driven Development

People writing proofs or programs in dependently typed languages can omit some function arguments in order to decrease the code size and improve readability. Type checking such a program involves filling in each of these implicit arguments in a type-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 33, Issue 5

May 1998

358 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/277652

Chairmen:
Jack W. Davidson
Univ. of Virginia
,
Keith D. Cooper
Rice Univ., Houston, TX
,
Editor:
A. Michael Berman
Rowan Univ., Glassboro, NJ

Issue’s Table of Contents

PLDI '98: Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation
May 1998
357 pages
ISBN:0897919874
DOI:10.1145/277650
Chairmen:
Jack W. Davidson
Univ. of Virginia
,
Keith D. Cooper
Rice Univ. Houston, TX
,
Editor:
A. Michael Berman
Rowan Univ. Glassboro, NJ

Copyright © 1998 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 1998

Published in SIGPLAN Volume 33, Issue 5

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

220
Total Citations
View Citations
1,183
Total Downloads

Downloads (Last 12 months)203
Downloads (Last 6 weeks)58

Reflects downloads up to 04 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Melquiond GMoreau J(2024)A Safe Low-Level Language for Computer Algebra and Its Formally Verified CompilerProceedings of the ACM on Programming Languages10.1145/36746298:ICFP(121-146)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674629
Economou DKrishnaswami NDunfield J(2023)Focusing on Refinement TypingACM Transactions on Programming Languages and Systems10.1145/3610408Online publication date: 17-Oct-2023
https://dl.acm.org/doi/10.1145/3610408
Hattori MKobayashi NSato R(2023)Gradual Tensor Shape CheckingProgramming Languages and Systems10.1007/978-3-031-30044-8_8(197-224)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_8
Al-Sibahi AJensen TDimovski AWąsowski A(2021)Verification of Program Transformations with Inductive Refinement TypesACM Transactions on Software Engineering and Methodology10.1145/340980530:1(1-33)Online publication date: 20-Jan-2021
https://dl.acm.org/doi/10.1145/3409805
Kawata AIgarashi A(2019)A Dependently Typed Multi-stage CalculusProgramming Languages and Systems10.1007/978-3-030-34175-6_4(53-72)Online publication date: 18-Nov-2019
https://doi.org/10.1007/978-3-030-34175-6_4
Kellogg MDort VMillstein SErnst MTip FBodden E(2018)Lightweight verification of array indexingProceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3213846.3213849(3-14)Online publication date: 12-Jul-2018
https://dl.acm.org/doi/10.1145/3213846.3213849
Schmid GKuncak VBiboudis AJonnalagedda MStucki SUreche V(2016)SMT-based checking of predicate-qualified types for ScalaProceedings of the 2016 7th ACM SIGPLAN Symposium on Scala10.1145/2998392.2998398(31-40)Online publication date: 30-Oct-2016
https://dl.acm.org/doi/10.1145/2998392.2998398
Kent AKempe DTobin-Hochstadt S(2016)Occurrence typing modulo theoriesACM SIGPLAN Notices10.1145/2980983.290809151:6(296-309)Online publication date: 2-Jun-2016
https://dl.acm.org/doi/10.1145/2980983.2908091
Cao CRen ZSchissler CManocha DZhou K(2016)Interactive sound propagation with bidirectional path tracingACM Transactions on Graphics10.1145/2980179.298243135:6(1-11)Online publication date: 5-Dec-2016
https://dl.acm.org/doi/10.1145/2980179.2982431
Du TSchulz AZhu BBickel BMatusik W(2016)Computational multicopter designACM Transactions on Graphics10.1145/2980179.298242735:6(1-10)Online publication date: 5-Dec-2016
https://dl.acm.org/doi/10.1145/2980179.2982427
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents