Paths: An Abstract Alternative to Pointers

Abstract

This paper introduces the path, a new programming language construct designed to supplant the use of pointers to access and destructively update recursive data structures. In contrast to the complex semantics and proof rules for pointers, the semantics and proof rules for paths are simple and abstract. In fact, they are easily formalized within a first-order theory of recursive data objects analogous to first-order number theory. We present a number of sample programs, including implementations of queues and binary trees, utilizing the new construct and prove that they are correct.