{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:37Z","timestamp":1779836737532,"version":"3.53.1"},"reference-count":64,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2013,10,22]],"date-time":"2013-10-22T00:00:00Z","timestamp":1382400000000},"content-version":"unspecified","delay-in-days":174,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2013,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>This paper presents a semantics of self-adjusting computation and proves that the semantics is correct and consistent. The semantics introduces memoizing change propagation, which enhances change propagation with the classic idea of memoization to enable reuse of computations even when memory is mutated via side effects. During evaluation, computation reuse via memoization triggers a change-propagation algorithm that adapts the reused computation to the memory mutations (side effects) that took place since the creation of the computation. Since the semantics includes both memoization and change propagation, it involves both non-determinism (due to memoization) and mutation (due to change propagation). Our consistency theorem states that the non-determinism is not harmful: any two evaluations of the same program starting at the same state yield the same result. Our correctness theorem states that mutation is not harmful: Self-adjusting programs are compatible with purely functional programming. We formalize the semantics and its meta-theory in the LF logical framework and machine check our proofs using Twelf.<\/jats:p>","DOI":"10.1017\/s0956796813000099","type":"journal-article","created":{"date-parts":[[2013,10,22]],"date-time":"2013-10-22T07:39:24Z","timestamp":1382427564000},"page":"249-292","source":"Crossref","is-referenced-by-count":4,"title":["A consistent semantics of self-adjusting computation"],"prefix":"10.1017","volume":"23","author":[{"given":"UMUT A.","family":"ACAR","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"MATTHIAS","family":"BLUME","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"JACOB","family":"DONHAM","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2013,10,22]]},"reference":[{"key":"S0956796813000099_ref64","doi-asserted-by":"publisher","DOI":"10.1145\/103135.103137"},{"key":"S0956796813000099_ref63","doi-asserted-by":"publisher","DOI":"10.1145\/507669.507654"},{"key":"S0956796813000099_ref12","doi-asserted-by":"crossref","unstructured":"Bhatotia P. , Wieder A. , Rodrigues R. , Acar U. A. , & Pasquini R. (2011) Incoop: MapReduce for incremental computations. In ACM Symposium on Cloud Computing.","DOI":"10.1145\/2038916.2038923"},{"key":"S0956796813000099_ref8","doi-asserted-by":"crossref","unstructured":"Acar U. A. , Blume M. & Donham J. (2007) A consistent semantics of self-adjusting computation. In European Symposium on Programming.","DOI":"10.1007\/978-3-540-71316-6_31"},{"key":"S0956796813000099_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)72018-4"},{"key":"S0956796813000099_ref9","doi-asserted-by":"crossref","unstructured":"Acar U. A. , Cotter A. , Hudson B. & T\u00fcrko\u011flu D. (2010) Dynamic well-spaced point sets. In Symposium on Computational Geometry.","DOI":"10.1145\/1810959.1811011"},{"key":"S0956796813000099_ref1","doi-asserted-by":"crossref","unstructured":"Abadi M. , Lampson B. W. & L\u00e9vy J.-J. (1996) Analysis and caching of dependencies. In International Conference on Functional Programming, pp. 83\u201391.","DOI":"10.1145\/232627.232638"},{"key":"S0956796813000099_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0056621"},{"key":"S0956796813000099_ref5","doi-asserted-by":"crossref","unstructured":"Acar U. A. , Blelloch G. E. & Harper R. (2003) Selective memoization. In Proceedings of the 30th Annual ACM Symposium on Principles of Programming Languages.","DOI":"10.1145\/604131.604133"},{"key":"S0956796813000099_ref22","volume-title":"Handbook on Data Structures and Applications","author":"Demetrescu","year":"2005"},{"key":"S0956796813000099_ref15","doi-asserted-by":"crossref","unstructured":"Carlsson M. (2002) Monads for incremental computing. In International Conference on Functional Programming, pp. 26\u201335.","DOI":"10.1145\/581478.581482"},{"key":"S0956796813000099_ref16","doi-asserted-by":"publisher","DOI":"10.1109\/5.163409"},{"key":"S0956796813000099_ref27","doi-asserted-by":"crossref","unstructured":"Field J. (November 1991) Incremental Reduction in the Lambda Calculus and Related Reduction Systems. PhD thesis, Department of Computer Science, Cornell University, Ithaca, NY.","DOI":"10.1145\/91556.91679"},{"key":"S0956796813000099_ref37","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006430"},{"key":"S0956796813000099_ref28","doi-asserted-by":"crossref","unstructured":"Field J. & Teitelbaum T. (1990) Incremental reduction in the lambda calculus. In ACM Conference LISP and Functional Programming, pp. 307\u2013322.","DOI":"10.1145\/91556.91679"},{"key":"S0956796813000099_ref51","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Proceedings of the 16th International Conference on Automated Deduction (CADE-16)","author":"Pfenning","year":"1999"},{"key":"S0956796813000099_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1596527.1596530"},{"key":"S0956796813000099_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63165-8_184"},{"key":"S0956796813000099_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/1186632.1186634"},{"key":"S0956796813000099_ref36","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"S0956796813000099_ref7","unstructured":"Acar U. A. , Blelloch G. E. , Harper R. , Vittes J. L. & Woo M. (2004) Dynamizing static algorithms with applications to dynamic trees and history independence. In ACM-SIAM Symposium on Discrete Algorithms, pp. 531\u2013540."},{"key":"S0956796813000099_ref11","volume-title":"Dynamic Programming","author":"Bellman","year":"1957"},{"key":"S0956796813000099_ref46","volume-title":"International Conference on Functional Programming","author":"Ley-Wild","year":"2008"},{"key":"S0956796813000099_ref44","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480907"},{"key":"S0956796813000099_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/265910.265914"},{"key":"S0956796813000099_ref33","doi-asserted-by":"crossref","unstructured":"Hammer M. A. , Acar U. A. & Chen Y. (2009) CEAL: A C-based language for self-adjusting computation. In ACM SIGPLAN Conference on Programming Language Design and Implementation.","DOI":"10.1145\/1542476.1542480"},{"key":"S0956796813000099_ref18","volume-title":"FrTime: Functional Reactive Programming in PLT Scheme","author":"Cooper","year":"2004"},{"key":"S0956796813000099_ref45","doi-asserted-by":"crossref","unstructured":"Ley-Wild R. , Acar U. A. & Fluet M. (2009) A cost semantics for self-adjusting computation. In Proceedings of the 26th Annual ACM Symposium on Principles of Programming Languages.","DOI":"10.1145\/1480881.1480907"},{"key":"S0956796813000099_ref13","unstructured":"Brodal G. S. & Jacob R. (2002) Dynamic planar convex hull. In Proceedings of the 43rd Annual IEEE Symposium on Foundations of Computer Science, pp 617\u2013626."},{"key":"S0956796813000099_ref59","first-page":"180","article-title":"Adaptive exact inference in graphical models","volume":"8","author":"S\u00fcmer","year":"2011","journal-title":"J. Mach. Learn."},{"key":"S0956796813000099_ref14","doi-asserted-by":"crossref","unstructured":"Burckhardt S. , Leijen D. , Sadowski C. , Yi J. & Ball T. (2011) Two for the price of one: A model for parallel and incremental computation. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications.","DOI":"10.1145\/2048066.2048101"},{"key":"S0956796813000099_ref17","unstructured":"Cohen R. F. & Tamassia R. (1991) Dynamic expression trees and their applications. In Proceedings of the 2nd Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 52\u201361."},{"key":"S0956796813000099_ref58","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3835"},{"key":"S0956796813000099_ref3","doi-asserted-by":"crossref","unstructured":"Acar U. A. , Ahmed A. & Blume M. (2008) Imperative self-adjusting computation. In Proceedings of the 25th Annual ACM Symposium on Principles of Programming Languages.","DOI":"10.1145\/1328438.1328476"},{"key":"S0956796813000099_ref56","doi-asserted-by":"crossref","unstructured":"Shankar A. & Bodik R. (2007) DITTO: Automatic incrementalization of data structure invariant checks (in Java). In International Conference on Programming Language Design and Implementation (PLDI).","DOI":"10.1145\/1250734.1250770"},{"key":"S0956796813000099_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/567532.567544"},{"key":"S0956796813000099_ref21","volume-title":"Handbook on Data Structures and Applications","author":"Demetrescu","year":"2005"},{"key":"S0956796813000099_ref2","unstructured":"Acar U. A. (May 2005) Self-Adjusting Computation. PhD thesis, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA."},{"key":"S0956796813000099_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/258948.258973"},{"key":"S0956796813000099_ref25","volume-title":"Algorithms and Theory of Computation Handbook","author":"Eppstein","year":"1999"},{"key":"S0956796813000099_ref29","doi-asserted-by":"publisher","DOI":"10.1137\/0214055"},{"key":"S0956796813000099_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(72)90045-2"},{"key":"S0956796813000099_ref19","doi-asserted-by":"crossref","unstructured":"Cooper G. H. & Krishnamurthi S. (2006) Embedding dynamic dataflow in a call-by-value language. In Proceedings of the 15th Annual European Symposium on Programming (ESOP).","DOI":"10.1007\/11693024_20"},{"key":"S0956796813000099_ref55","doi-asserted-by":"crossref","unstructured":"Reps T. (1982b) Optimal-time incremental semantic analysis for syntax-directed editors. In Proceedings of the 9th Annual Symposium on Principles of Programming Languages, pp. 169\u2013176.","DOI":"10.1145\/582153.582172"},{"key":"S0956796813000099_ref61","unstructured":"Tarjan R. & Werneck R. (2007) Dynamic trees in practice. In Proceedings of the 6th Workshop on Experimental Algorithms (WEA 2007), pp. 80\u201393."},{"key":"S0956796813000099_ref32","first-page":"1117","volume-title":"Handbook of Discrete and Computational Geometry","author":"Guibas","year":"2004"},{"key":"S0956796813000099_ref34","doi-asserted-by":"crossref","unstructured":"Hammer M. , Acar U. A. , Rajagopalan M. & Ghuloum A. (2007) A proposal for parallel self-adjusting computation. In DAMP '07: Workshop on Declarative Aspects of Multicore Programming.","DOI":"10.1145\/1248648.1248651"},{"key":"S0956796813000099_ref35","doi-asserted-by":"crossref","unstructured":"Hammer M. , Neis G. , Chen Y. & Acar U. A. (2011) Self-adjusting stack machines. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA).","DOI":"10.1145\/2048066.2048124"},{"key":"S0956796813000099_ref38","unstructured":"Hedin G. (March 1992) Incremental Semantics Analysis. PhD thesis, Department of Computer Science, Lund University, Lund, Sweden."},{"key":"S0956796813000099_ref57","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(83)90006-5"},{"key":"S0956796813000099_ref39","doi-asserted-by":"crossref","first-page":"594","DOI":"10.1007\/3-540-63165-8_214","volume-title":"ICALP '97: Proceedings of the 24th International Colloquium on Automata, Languages and Programming","author":"Henzinger","year":"1997"},{"key":"S0956796813000099_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349341"},{"key":"S0956796813000099_ref30","doi-asserted-by":"publisher","DOI":"10.1006\/jagm.1996.0835"},{"key":"S0956796813000099_ref43","unstructured":"Hoover R. (May 1987) Incremental Graph Evaluation. PhD thesis, Department of Computer Science, Cornell University, Ithaca, NY."},{"key":"S0956796813000099_ref47","doi-asserted-by":"publisher","DOI":"10.1145\/291889.291895"},{"key":"S0956796813000099_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/320211.320215"},{"key":"S0956796813000099_ref60","unstructured":"Sundaresh R. S. & Hudak P. (1991) Incremental compilation via partial evaluation. In Conference Record of the 18th Annual ACM Symposium on Principles of Programming Languages, pp. 1\u201313."},{"key":"S0956796813000099_ref49","doi-asserted-by":"publisher","DOI":"10.1038\/218019a0"},{"key":"S0956796813000099_ref42","doi-asserted-by":"publisher","DOI":"10.1145\/502090.502095"},{"key":"S0956796813000099_ref50","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90012-X"},{"key":"S0956796813000099_ref52","first-page":"315","volume-title":"16th Symposium on Principles of Programming Languages","author":"Pugh","year":"1989"},{"key":"S0956796813000099_ref53","doi-asserted-by":"crossref","unstructured":"Ramalingam G. & Reps T. (1993) A categorized bibliography on incremental computation. In Proceedings of the 20th Symposium on Principles of Programming Languages, pp. 502\u2013510.","DOI":"10.1145\/158511.158710"},{"key":"S0956796813000099_ref54","unstructured":"Reps T. (August 1982a) Generating Language-Based Environments. PhD thesis, Department of Computer Science, Cornell University, Ithaca, NY."},{"key":"S0956796813000099_ref62","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349331"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796813000099","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:05Z","timestamp":1779834965000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796813000099\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5]]},"references-count":64,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,5]]}},"alternative-id":["S0956796813000099"],"URL":"https:\/\/doi.org\/10.1017\/s0956796813000099","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,5]]}}}