{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:58:02Z","timestamp":1725663482644},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556022"},{"type":"electronic","value":"9783540472520"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_174","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T05:19:41Z","timestamp":1330233581000},"page":"310-324","source":"Crossref","is-referenced-by-count":4,"title":["Using middle-out reasoning to control the synthesis of tail-recursive programs"],"prefix":"10.1007","author":[{"given":"Jane","family":"Hesketh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Bundy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Smaill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"24_CR1","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic. Academic Press, 1979. ACM monograph series."},{"key":"24_CR2","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/BF00249016","volume":"7","author":"A. Bundy","year":"1991","unstructured":"A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Journal of Automated Reasoning, 7:303\u2013324, 1991. Earlier version available from Edinburgh as DAI Research Paper No 413.","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR3","unstructured":"A. Bundy, F. van Harmelen, J. Hesketh, A. Smaill, and A. Stevens. A rational reconstruction and extension of recursion analysis. In N.S. Sridharan, editor, Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, pages 359\u2013365, Morgan Kaufmann, 1989. Also available from Edinburgh as DAI Research Paper 419."},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 647\u2013648, Springer-Verlag, 1990. Lecture Notes in Artificial Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 507.","DOI":"10.1007\/3-540-52885-7_123"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"A. Bundy, F. van Harmelen, A. Smaill, and A. Ireland. Extensions to the rippling-out tactic for guiding inductive proofs. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 132\u2013146, Springer-Verlag, 1990. Lecture Notes in Artificial Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 459.","DOI":"10.1007\/3-540-52885-7_84"},{"issue":"3","key":"24_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(81)90014-X","volume":"16","author":"J. Darlington","year":"1981","unstructured":"J. Darlington. An experimental program transformation and synthesis system. Artificial Intelligence, 16(3):1\u201346, August 1981.","journal-title":"Artificial Intelligence"},{"key":"24_CR7","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G. Huet. A unification algorithm for lambda calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"24_CR8","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. Huet","year":"1978","unstructured":"G. Huet and B. Lang. Proving and applying program transformation expressed with second order patterns. Acta Informatica, 11:31\u201355, 1978.","journal-title":"Acta Informatica"},{"key":"24_CR9","unstructured":"D.J. Pym. Proofs, search and computation in general logic. PhD thesis, University of Edinburgh, 1990. Available as LFCS report ECS-LFCS-90-125."},{"key":"24_CR10","unstructured":"S.S. Wainer. Programs from proofs. 1989. Seminar given at the Department of Artificial Intelligence, Edinburgh."},{"key":"24_CR11","unstructured":"\u00c5Wikstr\u00f6m. Functional Programming Using Standard ML. Prentice Hall, 1987."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_174.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:32:55Z","timestamp":1619559175000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_174"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_174","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}