TY - GEN
T1 - Semi-persistent data structures
AU - Conchon, Sylvain
AU - Filliâtre, Jean Christophe
PY - 2008/7/21
Y1 - 2008/7/21
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-540-78739-6_25
DO - 10.1007/978-3-540-78739-6_25
M3 - Conference contribution
AN - SCOPUS:47249117594
SN - 3540787380
SN - 9783540787389
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 322
EP - 336
BT - Programming Languages and Systems - 17th European Symposium on Programming, ESOP 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings
T2 - 17th European Symposium on Programming, ESOP 2008
Y2 - 29 March 2008 through 6 April 2008
ER -