{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:45Z","timestamp":1775790765546,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466681","type":"print"},{"value":"9783662466698","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46669-8_17","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T18:37:37Z","timestamp":1427913457000},"page":"406-431","source":"Crossref","is-referenced-by-count":7,"title":["Refinement Types for Incremental Computational Complexity"],"prefix":"10.1007","author":[{"given":"Ezgi","family":"\u00c7i\u00e7ek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Umut","family":"Acar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"17_CR1","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.entcs.2005.11.043","volume":"148","author":"U. Acar","year":"2006","unstructured":"Acar, U., Blelloch, G., Blume, M., Harper, R., Tangwongsan, K.: A library for self-adjusting computation. Elec. Notes in Theor. Comp. Sci.\u00a0148(2), 127\u2013154 (2006)","journal-title":"Elec. Notes in Theor. Comp. Sci."},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Acar, U.A., Blelloch, G.E., Blume, M., Harper, R., Tangwongsan, K.: An experimental analysis of self-adjusting computation. ACM Trans. Program. Lang. Syst.\u00a03, 3:1\u20133:53 (2009)","DOI":"10.1145\/1596527.1596530"},{"issue":"6","key":"17_CR3","doi-asserted-by":"publisher","first-page":"990","DOI":"10.1145\/1186632.1186634","volume":"28","author":"U.A. Acar","year":"2006","unstructured":"Acar, U.A., Blelloch, G.E., Harper, R.: Adaptive functional programming. ACM Trans. Program. Lang. Syst.\u00a028(6), 990\u20131034 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Acar, U.A., Blume, M., Donham, J.: A consistent semantics of self-adjusting computation. The Journal of Functional Programming (2013)","DOI":"10.1017\/S0956796813000099"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/11693024_6","volume-title":"Programming Languages and Systems","author":"A. Ahmed","year":"2006","unstructured":"Ahmed, A.: Step-indexed syntactic logical relations for recursive and quantified types. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol.\u00a03924, pp. 69\u201383. Springer, Heidelberg (2006)"},{"issue":"1","key":"17_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jlap.2007.06.002","volume":"75","author":"B. Blanchet","year":"2008","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. The Journal of Logic and Algebraic Programming\u00a075(1), 3\u201351 (2008)","journal-title":"The Journal of Logic and Algebraic Programming"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Brodal, G.S., Jacob, R.: Dynamic planar convex hull. In: Proceedings of the 43rd Annual IEEE Symposium on Foundations of Computer Science, pp. 617\u2013626 (2002)","DOI":"10.1109\/SFCS.2002.1181985"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Carlsson, M.: Monads for incremental computing. In: Proceedings of the 7th International Conference on Functional Programming, ICFP 2002, pp. 26\u201335. ACM (2002)","DOI":"10.1145\/583852.581482"},{"issue":"8","key":"17_CR9","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/2240236.2240262","volume":"55","author":"S. Chaudhuri","year":"2012","unstructured":"Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity and robustness of programs. Communications of the ACM\u00a055(8), 107\u2013115 (2012)","journal-title":"Communications of the ACM"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Chen, Y., Dunfield, J., Acar, U.A.: Type-directed automatic incrementalization. In: Proceedings of the 33rd Conference on Programming Language Design and Implementation, PLDI 2012, pp. 299\u2013310. ACM (2012)","DOI":"10.1145\/2345156.2254100"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Chen, Y., Dunfield, J., Hammer, M.A., Acar, U.A.: Implicit self-adjusting computation for purely functional programs. In: International Conference on Functional Programming, ICFP 2011, pp. 129\u2013141 (2011)","DOI":"10.1145\/2034574.2034792"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Chin, W.N., Khoo, S.C.: Calculating sized types. In: Proceedings of the Workshop on Partial Evaluation and Semantics-based Program Manipulation, PEPM 2000, pp. 62\u201372. ACM (1999)","DOI":"10.1145\/328690.328893"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Dal Lago, U., Petit, B.: The geometry of types. In: Proceedings of the 40th Annual Symposium on Principles of Programming Languages, POPL 2013, pp. 167\u2013178. ACM (2013)","DOI":"10.1145\/2429069.2429090"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Demers, A., Reps, T., Teitelbaum, T.: Incremental evaluation for attribute grammars with application to syntax-directed editors. In: Proceedings of the 8th Symposium on Principles of Programming Languages, POPL 1981, pp. 105\u2013116. ACM (1981)","DOI":"10.1145\/567532.567544"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Field, J.: Incremental Reduction in the Lambda Calculus and Related Reduction Systems. Ph.D. thesis, Department of Computer Science, Cornell University (1991)","DOI":"10.1145\/91556.91679"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Gaboardi, M., Haeberlen, A., Hsu, J., Narayan, A., Pierce, B.C.: Linear dependent types for differential privacy. In: Proceedings of the 40th Annual Symposium on Principles of Programming Languages, POPL 2013, pp. 357\u2013370. ACM (2013)","DOI":"10.1145\/2480359.2429113"},{"issue":"4","key":"17_CR17","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1016\/0020-0190(72)90045-2","volume":"1","author":"R.L. Graham","year":"1972","unstructured":"Graham, R.L.: An efficient algorithm for determining the convex hull of a finite planar set. Information Processing Letters\u00a01(4), 132\u2013133 (1972)","journal-title":"Information Processing Letters"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.: Speed: Precise and efficient static estimation of program computational complexity. In: Proceedings of the 36th Annual Symposium on Principles of Programming Languages, POPL 2009, pp. 127\u2013139. ACM (2009)","DOI":"10.1145\/1480881.1480898"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Hammer, M.A., Acar, U.A., Chen, Y.: Ceal: A C-based language for self-adjusting computation. In: Proceedings of the 2009 Conference on Programming Language Design and Implementation, PLDI 2009, pp. 25\u201337. ACM (2009)","DOI":"10.1145\/1542476.1542480"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Hammer, M.A., Phang, K.Y., Hicks, M., Foster, J.S.: Adapton: Composable, demand-driven incremental computation. In: Proceedings of the 35th Conference on Programming Language Design and Implementation, PLDI 2014, pp. 156\u2013166. ACM (2014)","DOI":"10.1145\/2666356.2594324"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Heydon, A., Levin, R., Yu, Y.: Caching function calls using precise dependencies. In: Proceedings of the Conference on Programming Language Design and Implementation, PLDI 2000, pp. 311\u2013320. ACM (2000)","DOI":"10.1145\/358438.349341"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. In: Proceedings of the 38th Annual Symposium on Principles of Programming Languages, POPL 2011, pp. 357\u2013370. ACM (2011)","DOI":"10.1145\/1926385.1926427"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-11957-6_16","volume-title":"Programming Languages and Systems","author":"J. Hoffmann","year":"2010","unstructured":"Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential: A static inference of polynomial bounds for functional programs. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 287\u2013306. Springer, Heidelberg (2010)"},{"key":"17_CR24","unstructured":"Holm, J., de Lichtenberg, K.: Top-trees and dynamic graph algorithms. Tech. Rep. DIKU-TR-98\/17, Department of Computer Science, University of Copenhagen (1998)"},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L.: Recursion and dynamic data-structures in bounded space: Towards embedded ML programming. In: Proceedings of the Fourth International Conference on Functional Programming, ICFP 1999, pp. 70\u201381. ACM (1999)","DOI":"10.1145\/317765.317785"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Ley-Wild, R., Acar, U.A., Fluet, M.: A cost semantics for self-adjusting computation. In: Proceedings of the 36th Annual Symposium on Principles of Programming Languages, POPL 2009, pp. 186\u2013199. ACM (2009)","DOI":"10.1145\/1480881.1480907"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Ley-Wild, R., Fluet, M., Acar, U.A.: Compiling self-adjusting programs with continuations. In: Proceedings of the 13th International Conference on Functional Programming, ICFP 2008, pp. 321\u2013334. ACM (2008)","DOI":"10.1145\/1411204.1411249"},{"issue":"6","key":"17_CR28","doi-asserted-by":"publisher","first-page":"893","DOI":"10.1017\/S095679680500568X","volume":"15","author":"A. Nanevski","year":"2005","unstructured":"Nanevski, A., Pfenning, F.: Staged computation with names and necessity. J. Funct. Program.\u00a015(6), 893\u2013939 (2005)","journal-title":"J. Funct. Program."},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-48092-7_6","volume-title":"Correct System Design","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Riis Nielson, H.: Type and effect systems. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol.\u00a01710, pp. 114\u2013136. Springer, Heidelberg (1999)"},{"key":"17_CR30","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1016\/0022-0000(81)90012-X","volume":"23","author":"M.H. Overmars","year":"1981","unstructured":"Overmars, M.H., van Leeuwen, J.: Maintenance of configurations in the plane. Journal of Computer and System Sciences\u00a023, 166\u2013204 (1981)","journal-title":"Journal of Computer and System Sciences"},{"issue":"1","key":"17_CR31","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/596980.596983","volume":"25","author":"F. Pottier","year":"2003","unstructured":"Pottier, F., Simonet, V.: Information flow inference for ML. ACM Trans. Program. Lang. Syst.\u00a025(1), 117\u2013158 (2003)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Pugh, W., Teitelbaum, T.: Incremental computation via function caching. In: Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages, POPL 1989, pp. 315\u2013328. ACM (1989)","DOI":"10.1145\/75277.75305"},{"key":"17_CR33","doi-asserted-by":"crossref","unstructured":"Reed, J., Pierce, B.C.: Distance makes the types grow stronger: A calculus for differential privacy. In: Proceedings of the 15th International Conference on Functional Programming, ICFP 2010, pp. 157\u2013168. ACM (2010)","DOI":"10.1145\/1863543.1863568"},{"key":"17_CR34","doi-asserted-by":"crossref","unstructured":"Shankar, A., Bod\u00edk, R.: Ditto: Automatic incrementalization of data structure invariant checks (in Java). In: Proceedings of the Conference on Programming Language Design and Implementation, PLDI 2007, pp. 310\u2013319. ACM (2007)","DOI":"10.1145\/1250734.1250770"},{"key":"17_CR35","unstructured":"Vasconcelos, P.: Space cost analysis using sized types. Ph.D. thesis, School of Computer Science, University of St Andrews (2008)"},{"key":"17_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-27861-0_6","volume-title":"Implementation of Functional Languages","author":"P.B. Vasconcelos","year":"2005","unstructured":"Vasconcelos, P.B., Hammond, K.: Inferring cost equations for recursive, polymorphic and higher-order functional programs. In: Trinder, P., Michaelson, G.J., Pe\u00f1a, R. (eds.) IFL 2003. LNCS, vol.\u00a03145, pp. 86\u2013101. Springer, Heidelberg (2005)"},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of the 26th Symposium on Principles of Programming Languages, POPL 1999, pp. 214\u2013227. ACM (1999)","DOI":"10.1145\/292540.292560"},{"key":"17_CR38","doi-asserted-by":"crossref","unstructured":"Yellin, D., Strom, R.: Inc: A language for incremental computations. In: Proceedings of the Conference on Programming Language Design and Implementation, PLDI 1988, pp. 115\u2013124. ACM (1988)","DOI":"10.1145\/960116.54002"}],"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-662-46669-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T20:24:11Z","timestamp":1747859051000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46669-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466681","9783662466698"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46669-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}