Abstract
The need for direct memory manipulation through pointers is essential in many applications. However, it is also commonly understood that the use (or probably misuse) of pointers is often a rich source of program errors. Therefore, approaches that can effectively enforce safe use of pointers in programming are highly sought after. ATS is a programming language with a type system rooted in a recently developed framework Applied Type System, and a novel and desirable feature in ATS lies in its support for safe programming with pointers through a novel notion of stateful views. In particular, even pointer arithmetic is allowed in ATS and guaranteed to be safe by the type system of ATS. In this paper, we give an overview of this feature in ATS, presenting some interesting examples based on a prototype implementation of ATS to demonstrate the practicality of safe programming with pointer through stateful views.
Partially supported by NSF grant no. CCR-0229480
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Apt, K.R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs, xvi+441 pp. Springer, New York (1991); ISBN 0-387-97532-2 (New York) 3-540- 97532-2 (Berlin)
Constable, R.L., et al.: Implementing Mathematics with the NuPrl Proof Development System, x+299 pp. Prentice-Hall, Englewood Cliffs (1986) ISBN 0-13- 451832-2
Detlefs, D.: An overview of the extended static checking system. In: Workshop on Formal Methods in Software Practice (1996)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Fahndrich, M., Deline, R.: Adoption and Focus: Practical Linear Types for Imperative Programming. In: Proceedings of the ACM Conference on Programming Language Design and Implementation, Berlin, June 2002, pp. 13–24 (2002)
Foster, J., Terauchi, T., Aiken, A.: Flow-sensitive Type Qualifiers. In: ACM Conference on Programming Language Design and Implementation, Berlin, June 2002, pp. 1–12 (2002)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50(1), 1–101 (1987)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580, 583 (1969)
Jim, T., Morrisett, G., Grossman, D., Hicks, M., Baudet, M., Harris, M., Wang, Y.: Cyclone, a Safe Dialect of C (2001), http://www.cs.cornell.edu/Projects/cyclone/ , Available at http://www.cs.cornell.edu/Projects/cyclone/
Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, Uppsala, Sweden, September 2003, pp. 213–226 (2003)
Necula, G.C., McPeak, S., Weimer, W.: CCured: Type-Safe Retrofitting of Legacy Code. In: Proceedings of the 29th ACM Symposium on Principles of Programming Languages, London, January 2002, pp. 128–139 (2002)
Oiwa, Y., Sekiguchi, T., Sumii, E., Yonezawa, A.: Fail-safe ansi-c compiler: An approach to making c programs secure (progress report). In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol. 2609, pp. 133–153. Springer, Heidelberg (2003)
Reynolds, J.: Separation Logic: a logic for shared mutable data structures. In: Proceedings of 17th IEEE Symposium on Logic in Computer Science, LICS 2002 (2002), citeseer.nj.nec.com/reynolds02separation.html
Xi, H., Chen, C., Chen, G.: Guarded Recursive Datatype Constructors. In: Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages, New Orleans, LA, January 2003, pp. 224–235 (2003)
Xi, H., Harper, R.: A Dependently Typed Assembly Language. In: Proceedings of International Conference on Functional Programming, September 2001, pp. 169–180 (2001)
Xi, H.: Dependent Types in Practical Programming. PhD thesis, pp. viii+181–viii+189. Carnegie Mellon University (1998), Available at http://www.cs.cmu.edu/~hwxi/DML/thesis.ps
Xi, H.: Imperative Programming with Dependent Types. In: Proceedings of 15th IEEE Symposium on Logic in Computer Science, Santo Barbara, CA, June 2000, pp. 375–387 (2000)
Xi, H.: Applied Type System (July 2003), Available at http://www.cs.bu.edu/~hwxi/ATS
Xi, H.: Applied Type System (extended abstract). In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 394–408. Springer, Heidelberg (2004)
Xi, H., Pfenning, F.: Dependent Types in Practical Programming. In: Proceedings of 26th ACM SIGPLAN Symposium on Principles of Programming Languages, San Antonio, Texas, January 1999, pp. 214–227 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhu, D., Xi, H. (2005). Safe Programming with Pointers Through Stateful Views. In: Hermenegildo, M.V., Cabeza, D. (eds) Practical Aspects of Declarative Languages. PADL 2005. Lecture Notes in Computer Science, vol 3350. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30557-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-30557-6_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24362-5
Online ISBN: 978-3-540-30557-6
eBook Packages: Computer ScienceComputer Science (R0)