Guaranteeing Safe Destructive Updates Through a Type System with Uniqueness Information for Graphs

In this paper we present a type system for graph rewrite systems: uniqueness typing. It employs usage information to deduce whether an object is `unique' at a certain moment, i.e. is only locally accessible. In a type of a function it can be speci ed that the function requires a unique argument object. The correctness of type assignment guarantees that no external access on the original object will take place in the future. The presented type system is proven to be correct. We illustrate the power of the system by de ning an elegant quicksort algorithm that performs the sorting in situ on the data structure.

• Type: Conference
• Year: 1993
• Where: DAGSTUHL
• Authors: Sjaak Smetsers, Erik Barendsen, Marko C. J. D. van Eekelen, Marinus J. Plasmeijer
• Keywords: DAGSTUHL 1993, DAGSTUHL 2007, Graph Rewrite Systems, Type Assignment Guarantees, Unique Argument Object