{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:10:04Z","timestamp":1749125404076,"version":"3.41.0"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1999,1]]},"DOI":"10.1023\/a:1005969312327","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T00:10:48Z","timestamp":1040515848000},"page":"65-115","source":"Crossref","is-referenced-by-count":1,"title":["Recursive Program Optimization through Inductive Synthesis Proof Transformation"],"prefix":"10.1007","volume":"22","author":[{"given":"Peter","family":"Madden","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","reference":[{"key":"146987_CR1","unstructured":"Basin, David A.: Extracting circuits from constructive proofs, Research Paper 533, Dept. of Artificial Intelligence, Edinburgh, 1991. Also appeared in Proceedings of the IFIP-IEEE International Workshop on Formal Methods in VLSI Design, Miami, USA, 1991."},{"key":"146987_CR2","unstructured":"Bjerner, B.: Time Complexity of Programs in Type Theory, Ph.D. thesis, University of G\u00f6teborg, 1989."},{"key":"146987_CR3","unstructured":"Boyer, R. S. and Moore, J S.: A Computational Logic, Academic Press, 1979, ACMmonograph series."},{"key":"146987_CR4","unstructured":"Boyer, R. S. and Moore, J S.: A Computational Logic Handbook, Academic Press, 1988. Perspectives in Computing, Vol. 23."},{"key":"146987_CR5","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., van Harmelen, F. Ireland, A. and Smaill, A.: Rippling: A heuristic for guiding inductive proofs, Artificial Intelligence\n62 (1993), 185\u2013253. Also available from Edinburgh as DAI Research Paper 567.","journal-title":"Artificial Intelligence"},{"key":"146987_CR6","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/BF00249016","volume":"7","author":"A. Bundy","year":"1991","unstructured":"Bundy, A., van Harmelen, F., Hesketh, J. and Smaill, A.: Experiments with proof plans for induction, Journal of Automated Reasoning\n7 (1991), 303\u2013324. Earlier version available from Edinburgh as DAI Research Paper 413.","journal-title":"Journal of Automated Reasoning"},{"key":"146987_CR7","unstructured":"Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A. and Stevens, A.: A rational reconstruction and extension of recursion analysis, in N. S. Sridharan (ed.), Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, Morgan Kaufmann, 1989, pp. 359\u2013365. Also available from Edinburgh as DAI Research Paper 419."},{"key":"146987_CR8","doi-asserted-by":"crossref","unstructured":"Bundy, A., van Harmelen, F., Horn, C. and Smaill, A.: The Oyster-Clam system, in: M. E. Stickel (ed.), 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 449, Springer-Verlag, 1990, pp. 647\u2013648. Also available from Edinburgh as DAI Research Paper 507.","DOI":"10.1007\/3-540-52885-7_123"},{"issue":"1","key":"146987_CR9","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"R. M. Burstall","year":"1977","unstructured":"Burstall, R. M. and Darlington, J.: A transformation system for developing recursive programs, Journal of the Association for Computing Machinery\n24(1) (1977), 44\u201367.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"146987_CR10","unstructured":"Chin, W. N.: Automatic Methods for Program Transformation, Ph.D. thesis, Imperial College, 1990."},{"issue":"3","key":"146987_CR11","first-page":"265","volume":"5","author":"N. H. Cohen","year":"1983","unstructured":"Cohen, N. H.: Eliminating redundant recursive calls, ACM Transactions on Database Systems\n5(3) (1983), 265\u2013299.","journal-title":"ACM Transactions on Database Systems"},{"key":"146987_CR12","unstructured":"Curry, H. B. and Feys, R.: Combinatory Logic, North-Holland, 1958."},{"key":"146987_CR13","unstructured":"Darlington, J.: A Semantic Approach to Automatic Program Improvement, Ph.D. thesis, Dept. of Artificial Intelligence, Edinburgh, 1972."},{"issue":"3","key":"146987_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(81)90014-X","volume":"16","author":"J. Darlington","year":"1981","unstructured":"Darlington, J.: An experimental program transformation and synthesis system, Artificial Intelligence\n16(3) (1981), 1\u201346.","journal-title":"Artificial Intelligence"},{"key":"146987_CR15","doi-asserted-by":"crossref","unstructured":"Darlington, J.: A functional programming environment supporting execution, partial evaluation and transformation, in PARLE 1989, Eindhoven, Netherlands, 1989, pp. 286\u2013305.","DOI":"10.1007\/3540512845_46"},{"key":"146987_CR16","unstructured":"Howard, W. A.: The formulae-as-type notion of construction, in J. P. Seldin and J. R. Hindley (eds), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980, pp. 479\u2013490."},{"key":"146987_CR17","unstructured":"Lowe, H.: The use of theorem proving techniques in expert systems for configuration, in J.-C. Rault (ed.), Proceedings of the Eleventh International Workshop on Expert Systems and Their Applications, Avignon, EC2, May 1991. Also available from Edinburgh as DAI Research Paper 536."},{"key":"146987_CR18","unstructured":"Madden, P.: A NuPRL synthesis of several sorting algorithms: Towards an automatic program transformation system, Research Paper 356, Dept. of Artificial Intelligence, Edinburgh, 1987."},{"key":"146987_CR19","unstructured":"Madden, P.: The specialization and transformation of constructive existence proofs, in N. S. Sridharan (ed.), Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, Morgan Kaufmann, 1989. Also available as DAI Research Paper 416, Dept. of Artificial Intelligence, Edinburgh."},{"key":"146987_CR20","doi-asserted-by":"crossref","unstructured":"Madden, P.: Automated Program Transformation through Proof Transformation, Ph.D. thesis, University of Edinburgh, 1991.","DOI":"10.1007\/3-540-55602-8_183"},{"key":"146987_CR21","unstructured":"Madden, P.: Formal methods for automated program improvement, in B. Nebel and L. Dreschler-Fischer (ed.), KI-94: Advances in Artificial Intelligence. Proceedings of 18th German Annual Conference on Artificial Intelligence, Saarbrueken, Germany, September 1994, Springer-Verlag. A longer version is available from the Max-Planck-Institut as MPI-I\u201394\u201338."},{"key":"146987_CR22","unstructured":"Madden, P.: Linear to logarithmic optimization via proof transformation, Research paper MPII\u201394\u2013240, Max-Planck-Institute f\u00fcr Informatik, 1994."},{"issue":"1","key":"146987_CR23","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Manna, Z. and Waldinger, R.: A deductive approach to program synthesis, ACM Transactions on Programming Languages and Systems\n2(1) (1980), 90\u2013121.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"146987_CR24","first-page":"153","volume-title":"6th International Congress for Logic, Methodology and Philosophy of Science, Hanover, August 1979","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"Martin-L\u00f6f, Per: Constructive mathematics and computer programming, in 6th International Congress for Logic, Methodology and Philosophy of Science, Hanover, August 1979, pp. 153\u2013175. Republished by North-Holland, Amsterdam, 1982."},{"key":"146987_CR25","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1038\/218019a0","volume":"218","author":"D. Michie","year":"1968","unstructured":"Michie, D.: Memo functions and machine learning, Nature\n218 (1968), 19\u201322.","journal-title":"Nature"},{"key":"146987_CR26","doi-asserted-by":"crossref","unstructured":"Pettorossi, A.: A powerful strategy for deriving programs by transformation, in ACM Lisp and Functional Programming Conference, ACM, 1984, pp. 405\u2013426.","DOI":"10.1145\/800055.802044"},{"key":"146987_CR27","unstructured":"Stevens, A.: A rational reconstruction of Boyer and Moore' technique for constructing induction formulas, in Y. Kodratoff (ed.), The Proceedings of ECAI-88, European Conference on Artificial Intelligence, 1988, pp. 565\u2013570. Also available from Edinburgh as DAI Research Paper 360."},{"key":"146987_CR28","unstructured":"Tamaki, H. and Sato, T.: A transformation system for logic programs that preserves equivalence, Technical Report TR-018, ICOT, 1984."},{"key":"146987_CR29","unstructured":"Tamaki, H. and Sato, T.: A transformation system for logic programs which preserves equivalence, Technical Report, ICOT, 1983."},{"key":"146987_CR30","unstructured":"Wainer, S. S.: Logical and recursive complexity, Technical Report 31\/90 (Preprint Series), Center for Theoretical Computer Science, University of Leeds, 1990."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005969312327.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005969312327\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005969312327.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:35:52Z","timestamp":1749123352000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005969312327"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,1]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999,1]]}},"alternative-id":["146987"],"URL":"https:\/\/doi.org\/10.1023\/a:1005969312327","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1999,1]]}}}