Abstract
This paper is concerned with design, implementation and verification of persistent purely functional data structures which are motivated by the representation of natural numbers using positional number systems. A new implementation of random-access list based on redundant segmented binary numbers is described. It uses 4 digits and an invariant which guarantees constant worst-case bounds for cons, head, and tail list operations as well as logarithmic time for lookup and update. The relationship of random-access list with positional number system is formalized and benefits of this analogy are demonstrated.