Types for describing coordinated data structures

Coordinated data structures are sets of (perhaps unbounded) data structures where the nodes of each structure may share types with the corresponding nodes of the other structures. For example, consider a list of arguments, and a separate list of functions, where the n-th function of the second list should be applied only to the n-th argument of the first list. We can guarantee that this invariant is obeyed by coordinating the two lists, such that the type of the n-th argument is existentially quantified and identical to the argument type of the n-th function. In this paper, we describe a minimal set of features sufficient for a type system to support coordinated data structures. We also demonstrate that two known type systems (Crary and Weirich’s LX [6] and Xi, Chen and Chen’s guarded recursive datatypes [24]) have these features, even though the systems were developed for other purposes. We illustrate the power of coordinated data structures as a programming idiom with three ex...

• Type: Conference
• Year: 2005
• Where: TLDI
• Authors: Michael F. Ringenburg, Dan Grossman
• Keywords: Data Structures, Formal Methods, N-th Argument, N-th Function, TLDI 2005