{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:22:18Z","timestamp":1770286938854,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540787389","type":"print"},{"value":"9783540787396","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78739-6_25","type":"book-chapter","created":{"date-parts":[[2008,4,2]],"date-time":"2008-04-02T08:39:06Z","timestamp":1207125546000},"page":"322-336","source":"Crossref","is-referenced-by-count":3,"title":["Semi-persistent Data Structures"],"prefix":"10.1007","author":[{"given":"Sylvain","family":"Conchon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Christophe","family":"Filli\u00e2tre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"8","key":"25_CR1","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1145\/122598.122614","volume":"26","author":"H.G. Baker","year":"1991","unstructured":"Baker, H.G.: Shallow binding makes functional arrays fast. SIGPLAN Not.\u00a026(8), 145\u2013147 (1991)","journal-title":"SIGPLAN Not."},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"K. Mike Barnett","year":"2005","unstructured":"Mike Barnett, K., Leino, R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, Springer, Heidelberg (2005)"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Benedikt, M., Reps, T.W., Sagiv, S.: A decidable logic for describing linked data structures. In: European Symposium on Programming, pp. 2\u201319 (1999)","DOI":"10.1007\/3-540-49099-X_2"},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Escape analysis: Correctness proof, implementation and experimental results. In: Symposium on Principles of Programming Languages, pp. 25\u201337 (1998)","DOI":"10.1145\/268946.268949"},{"key":"25_CR5","unstructured":"Conchon, S., Contejean, E.: Ergo: A Decision Procedure for Program Verification, http:\/\/ergo.lri.fr\/"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Conchon, S., Filli\u00e2tre, J.-C.: A Persistent Union-Find Data Structure. In: ACM SIGPLAN Workshop on ML, Freiburg, Germany (October 2007)","DOI":"10.1145\/1292535.1292541"},{"key":"25_CR7","unstructured":"Conchon, S., Filli\u00e2tre, J.-C.: Semi-Persistent Data Structures. Research Report 1474, LRI, Universit\u00e9 Paris Sud (September 2007), http:\/\/www.lri.fr\/~filliatr\/ftp\/publis\/spds-rr.pdf"},{"key":"25_CR8","series-title":"Series in Automatic Computation","volume-title":"A discipline of programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A discipline of programming. Series in Automatic Computation. Prentice Hall Int., Englewood Cliffs (1976)"},{"issue":"1","key":"25_CR9","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1016\/0022-0000(89)90034-2","volume":"38","author":"J.R. Driscoll","year":"1989","unstructured":"Driscoll, J.R., Sarnak, N., Sleator, D.D., Tarjan, R.E.: Making Data Structures Persistent. Journal of Computer and System Sciences\u00a038(1), 86\u2013124 (1989)","journal-title":"Journal of Computer and System Sciences"},{"key":"25_CR10","unstructured":"Filli\u00e2tre, J.-C.: The Why verification tool, http:\/\/why.lri.fr\/"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification (Tool presentation). In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, Springer, Heidelberg (to appear, 2007)"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-60360-3_39","volume-title":"Static Analysis","author":"J. Hannan","year":"1995","unstructured":"Hannan, J.: A type-based analysis for stack allocation in functional languages. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol.\u00a0983, pp. 172\u2013188. Springer, Heidelberg (1995)"},{"key":"25_CR13","unstructured":"Knuth, D.E.: Dancing links. In: Davies, B.R.J., Woodcock, J. (eds.) Millennial Perspectives in Computer Science, Palgrave, pp. 187\u2013214 (2000)"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Morrisett, J.G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. In: Types in Compilation, pp. 28\u201352 (1998)","DOI":"10.21236\/ADA358572"},{"key":"25_CR15","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1145\/567067.567073","volume-title":"POPL 1983: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages","author":"G. Nelson","year":"1983","unstructured":"Nelson, G.: Verifying reachability invariants of linked structures. In: POPL 1983: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 38\u201347. ACM Press, New York (1983)"},{"key":"25_CR16","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511530104","volume-title":"Purely Functional Data Structures","author":"C. Okasaki","year":"1998","unstructured":"Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1998)"},{"key":"25_CR17","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1109\/SEFM.2006.7","volume-title":"SEFM 2006: Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods","author":"S. Ranise","year":"2006","unstructured":"Ranise, S., Zarba, C.: A theory of singly-linked lists and its extensible decision procedure. In: SEFM 2006: Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods, Washington, DC, USA, pp. 206\u2013215. IEEE Computer Society, Los Alamitos (2006)"},{"key":"25_CR18","first-page":"407","volume-title":"Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005)","author":"F. Spalding","year":"2005","unstructured":"Spalding, F., Walker, D.: Certifying compilation for a language with stack allocation. In: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), Washington, DC, USA, pp. 407\u2013416. IEEE Computer Society, Los Alamitos (2005)"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Tofte, M., Talpin, J.-P.: Implementation of the typed call-by-value lambda-calculus using a stack of regions. In: Symposium on Principles of Programming Languages, pp. 188\u2013201 (1994)","DOI":"10.1145\/174675.177855"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78739-6_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:20:50Z","timestamp":1619522450000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78739-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540787389","9783540787396"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78739-6_25","relation":{},"subject":[]}}