{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:10:24Z","timestamp":1742598624466,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540592938"},{"type":"electronic","value":"9783540492337"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59293-8_228","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:12:34Z","timestamp":1330276354000},"page":"681-695","source":"Crossref","is-referenced-by-count":8,"title":["Proving the correctness of recursion-based automatic program transformations"],"prefix":"10.1007","author":[{"given":"David","family":"Sands","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"45_CR1","unstructured":"S. Abramsky. The lazy lambda calculus. In Research Topics in Functional Programming. Addison Wesley, 1990."},{"key":"45_CR2","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"R. Burstall","year":"1977","unstructured":"R. Burstall and J. Darlington. A transformation system for developing recursive programs. JACM, 24:44\u201367, January 1977.","journal-title":"JACM"},{"key":"45_CR3","unstructured":"W. N. Chin. Automatic Methods for Program Transformation. PhD thesis, Imperial College, 1990."},{"key":"45_CR4","unstructured":"C. Consel and S. Khoo. On-line and off-line partial evaluation: Semantic specification and correctness proofs. Tech. Report, Yale, April 1993."},{"key":"45_CR5","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/BF01744293","volume":"13","author":"B. Courcelle","year":"1979","unstructured":"B. Courcelle. Infinite trees in normal form and recursive equations having a unique solution. Math. Systems Theory, 13:131\u2013180, 1979.","journal-title":"Math. Systems Theory"},{"key":"45_CR6","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/0304-3975(87)90109-5","volume":"52","author":"M. Felleisen","year":"1987","unstructured":"M. Felleisen, D. Friedman, and E. Kohlbecker. A syntactic theory of sequential control. TCS, 52:205\u2013237, 1987.","journal-title":"TCS"},{"key":"45_CR7","unstructured":"A. Ferguson and P. Wadler. When will deforestation stop. In 1988 Glasgow Workshop on Functional Programming, Research Rep. 89\/R4, 1988."},{"key":"45_CR8","doi-asserted-by":"crossref","unstructured":"R. Gl\u00fcck and A. V. Klimov. Occam's razor in metacomputation: the notion of a perfect process tree. In Static Analysis Syposium, LNCS 724, 1993.","DOI":"10.1007\/3-540-57264-3_34"},{"key":"45_CR9","doi-asserted-by":"crossref","unstructured":"A. Gill, J. Launchbury, and S. Peyton Jones. A short cut to deforestation. In FPCA '93. ACM Press, 1993.","DOI":"10.1145\/165180.165214"},{"issue":"2","key":"45_CR10","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1145\/128861.128864","volume":"14","author":"C. Gomard","year":"1992","unstructured":"C. Gomard. A self-applicable partial evaluator for the lambda calculus: correctness and pragmatics. ACM TOPLAS, 14(2):147\u2013172, 1992.","journal-title":"ACM TOPLAS"},{"key":"45_CR11","unstructured":"D. J. Howe. Equality in lazy computation systems. In 4th LICS. IEEE, 1989."},{"key":"45_CR12","unstructured":"N. D. Jones, C. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall, 1993."},{"key":"45_CR13","doi-asserted-by":"crossref","unstructured":"J. Komorowski. An introduction to partial deduction. In Third Int. Workshop on Meta-Programming in Logic, LNCS 649, 1992.","DOI":"10.1007\/3-540-56282-6_4"},{"key":"45_CR14","unstructured":"L. Kott. About transformation system: A theoretical study. In B. Robinet, editor, Program Transformations. Dunod, 1978."},{"key":"45_CR15","doi-asserted-by":"crossref","unstructured":"J. W. Lloyd and J. Shepherdson. Partial evaluation in logic programming. J. Logic Programming, 3\u20134(11), 1991.","DOI":"10.1016\/0743-1066(91)90027-M"},{"key":"45_CR16","doi-asserted-by":"crossref","unstructured":"S. Marlow and P. Wadler. Deforestation for higher-order functions. In Functional Programming, Glasgow 1992, Springer Workshop Series, 1992.","DOI":"10.1007\/978-1-4471-3215-8_14"},{"key":"45_CR17","volume-title":"S\u00f8rensen Deforestation, partial exaluation and evaluation orders","author":"K. Nielsen","year":"1994","unstructured":"K. Nielsen and M. Heine S\u00f8rensen Deforestation, partial exaluation and evaluation orders. Unpublished, DIKU, Copenhagen, 1994."},{"key":"45_CR18","doi-asserted-by":"crossref","unstructured":"J. Palsberg. Correctness of binding time analysis. J. Functional Programming, 3(3), 1993.","DOI":"10.1017\/S0956796800000770"},{"issue":"1","key":"45_CR19","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G. D. Plotkin","year":"1975","unstructured":"G. D. Plotkin. Call-by-name, Call-by-value and the \u03bb-calculus. TCS, 1(1):125\u2013159, 1975.","journal-title":"TCS"},{"key":"45_CR20","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1145\/356914.356917","volume":"15","author":"P. Partsch","year":"1983","unstructured":"P. Partsch and R. Steinbruggen. Program transformation systems. Computing Surveys, 15:199\u2013236, 1983.","journal-title":"Computing Surveys"},{"key":"45_CR21","doi-asserted-by":"crossref","unstructured":"D. Sands. Operational theories of improvement in functional languages (extended abstract). In Fourth Glasgow Workshop on Functional Programming, Springer Workshop Series, 1991.","DOI":"10.1007\/978-1-4471-3196-0_24"},{"key":"45_CR22","doi-asserted-by":"crossref","unstructured":"D. Sands. Total correctness by local improvement in program transformation. In 22nd POPL. ACM Press, 1995.","DOI":"10.1145\/199448.199485"},{"key":"45_CR23","doi-asserted-by":"crossref","unstructured":"D. Sands. Total correctness by local improvement in the transformation of functional programs. DIKU, University of Copenhagen, 48pages, January 1995.","DOI":"10.1145\/199448.199485"},{"key":"45_CR24","doi-asserted-by":"crossref","unstructured":"T. Sheard and L. Fegaras. A fold for all seasons. In FPCA '93. ACM Press, 1993.","DOI":"10.1145\/165180.165216"},{"key":"45_CR25","doi-asserted-by":"crossref","unstructured":"M. H. S\u00f8rensen, R. Gl\u00fcck, and N. D. Jones. Towards unifying partial evaluation, deforestation, supercompilation, and GPC. In ESOP'94. LNCS 788, Springer Verlag, 1994.","DOI":"10.1007\/3-540-57880-3_32"},{"key":"45_CR26","unstructured":"M H S\u00f8rensen. A grammar-based data-flow analysis to stop deforestation. In CAAP'94, LNCS 787, 1994."},{"key":"45_CR27","unstructured":"M H S\u00f8rensen. Turchin's supercompiler revisited: An operational theory of positive information propagation. Master's thesis, DIKU, University of Copenhagen, (RR 94\/9) 1994."},{"key":"45_CR28","volume-title":"PhD thesis","author":"P. Steckler","year":"1994","unstructured":"P. Steckler. Correct Higher-Order Program Transformations. PhD thesis, Northeastern University, Boston, 1994."},{"key":"45_CR29","unstructured":"H. Tamaki and T. Sato. Unfold\/fold transformation of logic programs. In 2nd Int. Logic Programming Conf., 1984."},{"key":"45_CR30","first-page":"292","volume":"8","author":"V. F. Turchin","year":"1986","unstructured":"V. F. Turchin. The concept of a supercompiler. To PLaS, 8:292\u2013325, July 1986.","journal-title":"To PLaS"},{"key":"45_CR31","unstructured":"P. Wadler. The concatenate vanishes. University of Glasgow. Unpublished (preliminary version circulated on the fp mailing list, 1987), November 1989."},{"key":"45_CR32","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0304-3975(90)90147-A","volume":"73","author":"P. Wadler","year":"1990","unstructured":"P. Wadler. Deforestation: transforming programs to eliminate trees. TCS, 73:231\u2013248, 1990. (Preliminary version in ESOP 88, LNCS 300).","journal-title":"TCS"},{"key":"45_CR33","doi-asserted-by":"crossref","unstructured":"M. Wand. Specifying the correctness of binding time analysis. J. Functional Programming, 3(3), 1993.","DOI":"10.1017\/S0956796800000782"}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '95: Theory and Practice of Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59293-8_228.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:45:33Z","timestamp":1742597133000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59293-8_228"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540592938","9783540492337"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-59293-8_228","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}