{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T13:31:30Z","timestamp":1725975090624},"publisher-location":"Cham","reference-count":10,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319897189"},{"type":"electronic","value":"9783319897196"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89719-6_7","type":"book-chapter","created":{"date-parts":[[2018,4,18]],"date-time":"2018-04-18T14:44:21Z","timestamp":1524062661000},"page":"118-134","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Automatically Introducing Tail Recursion in\u00a0CakeML"],"prefix":"10.1007","author":[{"given":"Oskar","family":"Abrahamsson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,19]]},"reference":[{"issue":"1","key":"7_CR1","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"RM Burstall","year":"1977","unstructured":"Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. J. ACM (JACM) 24(1), 44\u201367 (1977)","journal-title":"J. ACM (JACM)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/10722298_2","volume-title":"Implementation of Functional Languages","author":"O Chitil","year":"2000","unstructured":"Chitil, O.: Type-inference based short cut deforestation (nearly) without inlining. In: Koopman, P., Clack, C. (eds.) IFL 1999. LNCS, vol. 1868, pp. 19\u201335. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/10722298_2"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/3-540-45127-7_13","volume-title":"Rewriting Techniques and Applications","author":"A K\u00fchnemann","year":"2001","unstructured":"K\u00fchnemann, A., Gl\u00fcck, R., Kakehi, K.: Relating accumulative and non-accumulative functional programs. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 154\u2013168. Springer, Heidelberg (2001). \nhttps:\/\/doi.org\/10.1007\/3-540-45127-7_13"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Principles of Programming Languages (POPL). ACM (2014)","DOI":"10.1145\/2535838.2535841"},{"issue":"11","key":"7_CR5","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/328691.328700","volume":"34","author":"YA Liu","year":"1999","unstructured":"Liu, Y.A., Stoller, S.D.: From recursion to iteration: what are the optimizations? ACM Sigplan Not. 34(11), 73\u201382 (1999)","journal-title":"ACM Sigplan Not."},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/978-3-662-49498-1_23","volume-title":"Programming Languages and Systems","author":"S Owens","year":"2016","unstructured":"Owens, S., Myreen, M.O., Kumar, R., Tan, Y.K.: Functional big-step semantics. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 589\u2013615. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49498-1_23"},{"issue":"ICFP","key":"7_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3110262","volume":"1","author":"Scott Owens","year":"2017","unstructured":"Owens, S., Norrish, M., Kumar, R., Myreen, M.O., Tan, Y.K.: Verifying efficient function calls in CakeML. In: International Conference on Functional Programming (ICFP). ACM Press, September 2017","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Tan, Y.K., Myreen, M.O., Kumar, R., Fox, A., Owens, S., Norrish, M.: A new verified compiler backend for CakeML. In: International Conference on Functional Programming (ICFP). ACM Press (2016)","DOI":"10.1145\/2951913.2951924"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Tan, Y.K., Owens, S., Kumar, R.: A verified type system for CakeML. In: Implementation and Application of Functional Programming Languages (IFL), p. 7. ACM (2015)","DOI":"10.1145\/2897336.2897344"},{"key":"7_CR10","unstructured":"Wadler, P.: The concatenate vanishes. Note, University of Glasgow (1987)"}],"container-title":["Lecture Notes in Computer Science","Trends in Functional Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89719-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,4,18]],"date-time":"2018-04-18T14:47:28Z","timestamp":1524062848000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89719-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319897189","9783319897196"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89719-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}