Semi-persistent Data Structures

A data structure is said to be persistent when any update operation returns a new structure without altering the old version. This paper introduces a new notion of persistence, called semi-persistence, where only ancestors of the most recent version can be accessed or updated. Making a data structure semi-persistent may improve its time and space complexity. This is of particular interest in backtracking algorithms manipulating persistent data structures, where this property is usually satisfied. We propose a proof system to statically check the valid use of semi-persistent data structures. It requires a few annotations from the user and then generates proof obligations that are automatically discharged by a dedicated decision procedure.

• Type: Conference
• Year: 2008
• Where: ESOP
• Authors: Sylvain Conchon, Jean-Christophe Filliâtre
• Keywords: Data Structures, ESOP 2008, Persistent Data Structures, Programming Languages, Semi-persistent Data Structures