{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T03:34:29Z","timestamp":1725680069006},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642297083"},{"type":"electronic","value":"9783642297090"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29709-0_15","type":"book-chapter","created":{"date-parts":[[2012,5,12]],"date-time":"2012-05-12T09:49:34Z","timestamp":1336816174000},"page":"153-169","source":"Crossref","is-referenced-by-count":2,"title":["Proving the Correctness of Unfold\/Fold Program Transformations Using Bisimulation"],"prefix":"10.1007","author":[{"given":"Geoff W.","family":"Hamilton","sequence":"first","affiliation":[]},{"given":"Neil D.","family":"Jones","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Abramsky, S.: The lazy lambda calculus. In: Research Topics in Functional Programming, pp. 65\u2013116. Addison-Wesley (1990)"},{"issue":"1-2","key":"15_CR2","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0743-1066(93)90022-9","volume":"16","author":"R. Bol","year":"1993","unstructured":"Bol, R.: Loop Checking in Partial Deduction. Journal of Logic Programming\u00a016(1-2), 25\u201346 (1993)","journal-title":"Journal of Logic Programming"},{"issue":"1","key":"15_CR3","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"R. Burstall","year":"1977","unstructured":"Burstall, R., Darlington, J.: A transformation system for developing recursive programs. Journal of the ACM\u00a024(1), 44\u201367 (1977)","journal-title":"Journal of the ACM"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite Systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 243\u2013320. Elsevier, MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"issue":"1-2","key":"15_CR5","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0304-3975(98)00353-3","volume":"228","author":"A.D. Gordon","year":"1999","unstructured":"Gordon, A.D.: Bisimilarity as a theory of functional programming. Theoretical Computer Science\u00a0228(1-2), 5\u201347 (1999)","journal-title":"Theoretical Computer Science"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Hamilton, G.: Distillation: Extracting the Essence of Programs. In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 61\u201370 (2007)","DOI":"10.1145\/1244381.1244391"},{"key":"15_CR7","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"2","author":"G. Higman","year":"1952","unstructured":"Higman, G.: Ordering by Divisibility in Abstract Algebras. Proceedings of the London Mathematical Society\u00a02, 326\u2013336 (1952)","journal-title":"Proceedings of the London Mathematical Society"},{"issue":"2","key":"15_CR8","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1006\/inco.1996.0008","volume":"124","author":"D.J. Howe","year":"1996","unstructured":"Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Information and Computation\u00a0124(2), 103\u2013112 (1996)","journal-title":"Information and Computation"},{"key":"15_CR9","unstructured":"Jones, N., Gomard, C., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall (1993)"},{"key":"15_CR10","first-page":"210","volume":"95","author":"J. Kruskal","year":"1960","unstructured":"Kruskal, J.: Well-Quasi Ordering, the Tree Theorem, and Vazsonyi\u2019s Conjecture. Transactions of the American Mathematical Society\u00a095, 210\u2013225 (1960)","journal-title":"Transactions of the American Mathematical Society"},{"issue":"3","key":"15_CR11","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1023\/B:LISP.0000029444.99264.c0","volume":"17","author":"D. Lacey","year":"2004","unstructured":"Lacey, D., Jones, N.D., Wyk, E.V., Frederiksen, C.C.: Compiler optimization correctness by temporal logic. Higher-Order and Symbolic Computation\u00a017(3), 173\u2013206 (2004)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Leuschel, M.: On the Power of Homeomorphic Embedding for Online Termination. In: Proceedings of the International Static Analysis Symposium, Pisa, Italy, pp. 230\u2013245 (1998)","DOI":"10.1007\/3-540-49727-7_14"},{"key":"15_CR13","unstructured":"Marlet, R.: Vers une Formalisation de l\u2019\u00c9valuation Partielle. Ph.D. thesis, Universit\u00e9 de Nice - Sophia Antipolis (1994)"},{"issue":"1-2","key":"15_CR14","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/0304-3975(96)00074-6","volume":"167","author":"D. Sands","year":"1996","unstructured":"Sands, D.: Proving the Correctness of Recursion-Based Automatic Program Transformations. Theoretical Computer Science\u00a0167(1-2), 193\u2013233 (1996)","journal-title":"Theoretical Computer Science"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/BFb0017492","volume-title":"Trees in Algebra and Programming - CAAP \u201994","author":"M.H. S\u00f8rensen","year":"1994","unstructured":"S\u00f8rensen, M.H., Gl\u00fcck, R.: An Algorithm of Generalization in Positive Supercompilation. In: Tison, S. (ed.) CAAP 1994. LNCS, vol.\u00a0787, pp. 335\u2013351. Springer, Heidelberg (1994)"},{"issue":"6","key":"15_CR16","doi-asserted-by":"publisher","first-page":"811","DOI":"10.1017\/S0956796800002008","volume":"6","author":"M.H. S\u00f8rensen","year":"1996","unstructured":"S\u00f8rensen, M.H., Gl\u00fcck, R., Jones, N.: A Positive Supercompiler. Journal of Functional Programming\u00a06(6), 811\u2013838 (1996)","journal-title":"Journal of Functional Programming"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/3-540-16446-4_15","volume-title":"Programs as Data Objects","author":"V. Turchin","year":"1986","unstructured":"Turchin, V.: Program Transformation by Supercompilation. In: Ganzinger, H., Jones, N.D. (eds.) Programs as Data Objects. LNCS, vol.\u00a0217, pp. 257\u2013281. Springer, Heidelberg (1986)"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/3-540-19027-9_23","volume-title":"ESOP \u201988","author":"P. Wadler","year":"1988","unstructured":"Wadler, P.: Deforestation: Transforming Programs to Eliminate Trees. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol.\u00a0300, pp. 344\u2013358. Springer, Heidelberg (1988)"}],"container-title":["Lecture Notes in Computer Science","Perspectives of Systems Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29709-0_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:14:17Z","timestamp":1620126857000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-29709-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642297083","9783642297090"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29709-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}