{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:26:45Z","timestamp":1784255205355,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642171635","type":"print"},{"value":"9783642171642","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-17164-2_13","type":"book-chapter","created":{"date-parts":[[2010,11,19]],"date-time":"2010-11-19T05:54:39Z","timestamp":1290146079000},"page":"172-187","source":"Crossref","is-referenced-by-count":19,"title":["Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics"],"prefix":"10.1007","author":[{"given":"Jan","family":"Hoffmann","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Hofmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Jost, S.: Static Prediction of Heap Space Usage for First-Order Functional Programs. In: 30th ACM Symp. on Principles of Prog. Langs. (POPL 2003), pp. 185\u2013197 (2003)","DOI":"10.1145\/604131.604148"},{"issue":"2","key":"13_CR2","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1137\/0606031","volume":"6","author":"R.E. Tarjan","year":"1985","unstructured":"Tarjan, R.E.: Amortized Computational Complexity. SIAM J. Algebraic Discrete Methods\u00a06(2), 306\u2013318 (1985)","journal-title":"SIAM J. Algebraic Discrete Methods"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/11693024_3","volume-title":"Programming Languages and Systems","author":"M. Hofmann","year":"2006","unstructured":"Hofmann, M., Jost, S.: Type-Based Amortised Heap-Space Analysis. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol.\u00a03924, pp. 22\u201337. Springer, Heidelberg (2006)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-04027-6_24","volume-title":"Computer Science Logic","author":"M. Hofmann","year":"2009","unstructured":"Hofmann, M., Rodriguez, D.: Efficient Type-Checking for Amortised Heap-Space Analysis. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol.\u00a05771, pp. 317\u2013331. Springer, Heidelberg (2009)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-05089-3_23","volume-title":"FM 2009: Formal Methods","author":"S. Jost","year":"2009","unstructured":"Jost, S., Loidl, H.W., Hammond, K., Scaife, N., Hofmann, M.: Carbon Credits for Resource-Bounded Computations using Amortised Analysis. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 354\u2013369. Springer, Heidelberg (2009)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-642-00590-9_14","volume-title":"Programming Languages and Systems","author":"B. Campbell","year":"2009","unstructured":"Campbell, B.: Amortised Memory Analysis using the Depth of Data Structures. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 190\u2013204. Springer, Heidelberg (2009)"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Jost, S., Hammond, K., Loidl, H.W., Hofmann, M.: Static Determination of Quantitative Resource Usage for Higher-Order Programs. In: 37th ACM Symp. on Principles of Prog. Langs. (POPL 2010), pp. 223\u2013236 (2010)","DOI":"10.1145\/1706299.1706327"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-11957-6_6","volume-title":"Programming Languages and Systems","author":"R. Atkey","year":"2010","unstructured":"Atkey, R.: Amortised Resource Analysis with Separation Logic. In: Gordon, A.D. (ed.) Programming Languages and Systems. LNCS, vol.\u00a06012, pp. 85\u2013103. Springer, Heidelberg (2010)"},{"key":"13_CR9","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. In: Gordon, A.D. (ed.) Programming Languages and Systems. LNCS, vol.\u00a06012, pp. 287\u2013306. Springer, Heidelberg (2010)"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Inductive Definitions, Semantics and Abstract Interpretations. In: 19th ACM Symp. on Principles of Prog. Langs. (POPL 1992), pp. 83\u201394 (1992)","DOI":"10.1145\/143165.143184"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/11693024_5","volume-title":"Programming Languages and Systems","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Coinductive Big-Step Operational Semantics. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol.\u00a03924, pp. 54\u201368. Springer, Heidelberg (2006)"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Grobauer, B.: Cost Recurrences for DML Programs. In: 6th Intl. Conf. on Funct. Prog. (ICFP 2001), pp. 253\u2013264 (2001)","DOI":"10.1145\/507635.507666"},{"issue":"1","key":"13_CR13","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0304-3975(91)90145-R","volume":"79","author":"P. Flajolet","year":"1991","unstructured":"Flajolet, P., Salvy, B., Zimmermann, P.: Automatic Average-case Analysis of Algorithms. Theoret. Comput. Sci.\u00a079(1), 37\u2013109 (1991)","journal-title":"Theoret. Comput. Sci."},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Crary, K., Weirich, S.: Resource Bound Certification. In: 27th ACM Symp. on Principles of Prog. Langs. (POPL 2000), pp. 184\u2013198 (2000)","DOI":"10.1145\/325694.325716"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-71316-6_12","volume-title":"Programming Languages and Systems","author":"E. Albert","year":"2007","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost Analysis of Java Bytecode. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 157\u2013172. Springer, Heidelberg (2007)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/978-3-540-69166-2_15","volume-title":"15th Symp. Stat. An. (SAS 2008)","author":"E. Albert","year":"2008","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol.\u00a05079, pp. 221\u2013237. Springer, Heidelberg (2008)"},{"issue":"1-2","key":"13_CR17","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.tcs.2003.10.022","volume":"318","author":"R. Benzinger","year":"2004","unstructured":"Benzinger, R.: Automated Higher-Order Complexity Analysis. Theor. Comput. Sci.\u00a0318(1-2), 79\u2013103 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.M.: SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In: 36th ACM Symp. on Principles of Prog. Langs. (POPL 2009), pp. 127\u2013139 (2009)","DOI":"10.1145\/1480881.1480898"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-540-70545-1_35","volume-title":"Comp. Aid. Verification, 20th Int. Conf. (CAV 2008)","author":"B.S. Gulavani","year":"2008","unstructured":"Gulavani, B.S., Gulwani, S.: A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 370\u2013384. Springer, Heidelberg (2008)"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Zuleger, F.: The Reachability-Bound Problem. In: Conf. on Prog. Lang. Design and Impl. (PLDI 2010), pp. 292\u2013304 (2010)","DOI":"10.1145\/1806596.1806630"},{"key":"13_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-540-32275-7_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"L. Beringer","year":"2005","unstructured":"Beringer, L., Hofmann, M., Momigliano, A., Shkaravska, O.: Automatic Certification of Heap Consumption. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 347\u2013362. Springer, Heidelberg (2005)"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L., Sabry, A.: Proving the Correctness of Reactive Systems Using Sized Types. In: Symp. Princ. of Prog. Langs. (POPL 1996), pp. 410\u2013423 (1996)","DOI":"10.1145\/237721.240882"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L.: Recursion and Dynamic Data-structures in Bounded Space: Towards Embedded ML Programming. In: 4th Intl. Conf. on Funct. Prog. (ICFP 1999), pp. 70\u201381 (1999)","DOI":"10.1145\/317765.317785"},{"issue":"2-3","key":"13_CR24","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1023\/A:1012996816178","volume":"14","author":"W.N. Chin","year":"2001","unstructured":"Chin, W.N., Khoo, S.C.: Calculating Sized Types. High.-Ord. and Symb. Comp. High.-Ord. and Symb. Comp.\u00a014(2-3), 261\u2013300 (2001)","journal-title":"High.-Ord. and Symb. Comp."},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-540-73228-0_25","volume-title":"Typed Lambda Calculi and Applications","author":"O. Shkaravska","year":"2007","unstructured":"Shkaravska, O., van Kesteren, R., van Eekelen, M.C.: Polynomial Size Analysis of First-Order Functions. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol.\u00a04583, pp. 351\u2013365. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17164-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T07:18:14Z","timestamp":1559805494000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17164-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642171635","9783642171642"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17164-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}