{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:41:26Z","timestamp":1750308086678,"version":"3.41.0"},"reference-count":93,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2005,11,1]],"date-time":"2005-11-01T00:00:00Z","timestamp":1130803200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2005,11]]},"abstract":"<jats:p>Recent research suggests that the goal of fully automatic and reliable program generation for a broad range of applications is coming nearer to feasibility. However, several interesting and challenging problems remain to be solved before it becomes a reality. Solving them is also<jats:italic>necessary,<\/jats:italic>if we hope ever to elevate software engineering from its current state (a highly developed handiwork) into a successful branch of engineering, capable of solving a wide range of new problems by systematic, well-automated and well-founded methods.A key problem in all program generation is<jats:italic>termination<\/jats:italic>of the generation process. This article focuses on off-line partial evaluation and describes recent progress towards automatically solving the termination problem, first for individual programs, and then for specializers and \u201cgenerating extensions,\u201d the program generators that most offline partial evaluators produce.The technique is based on<jats:italic>size-change graphs<\/jats:italic>that approximate the changes in parameter sizes at function calls. We formulate a criterion,<jats:italic>bounded anchoring,<\/jats:italic>for detecting parameters known to be bounded during specialization: a bounded parameter can act as an<jats:italic>anchor<\/jats:italic>for other parameters. Specialization points necessary for termination are computed by adding a parameter that tracks call depth, and then selecting a specialization point in every call loop where it is unanchored. By generalizing all unbounded parameters, we compute a binding-time division which together with the set of specialization points<jats:italic>guarantees<\/jats:italic>termination.Contributions of this article include a proof, based on the operational semantics of partial evaluation with memoization, that the analysis guarantees termination; and an in-depth description of safety of the increasing size approximation operator required for termination analysis in partial evaluation.Initial experiments with a prototype shows that the analysis overall yields binding-time divisions that can achieve a high degree of specialization, while still guaranteeing termination.The article ends with a list of challenging problems whose solution would bring the community closer to the goal of broad-spectrum, fully automatic and reliable program generation.<\/jats:p>","DOI":"10.1145\/1108970.1108973","type":"journal-article","created":{"date-parts":[[2006,2,6]],"date-time":"2006-02-06T15:07:09Z","timestamp":1139238429000},"page":"1147-1215","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Termination analysis and specialization-point insertion in offline partial evaluation"],"prefix":"10.1145","volume":"27","author":[{"given":"Arne John","family":"Glenstrup","sequence":"first","affiliation":[{"name":"IT University of Copenhagen, Copenhagen S, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neil D.","family":"Jones","sequence":"additional","affiliation":[{"name":"DIKU, University of Copenhagen, Copenhagen \u00f8, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,11]]},"reference":[{"volume-title":"Abstracts of the Fourth International Workshop on Termination WST'99","author":"Abel A.","key":"e_1_2_1_1_1","unstructured":"Abel , A. and Altenkirch , T . 1999. A semantical analysis of structural recursion . In Abstracts of the Fourth International Workshop on Termination WST'99 . unpublished (Dagstuhl, Germany), 24--25.]] Abel, A. and Altenkirch, T. 1999. A semantical analysis of structural recursion. In Abstracts of the Fourth International Workshop on Termination WST'99. unpublished (Dagstuhl, Germany), 24--25.]]"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1177220"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 3rd International Static Analysis Symposium (SAS), R. Cousot and D. A. Schmidt, Eds. Lecture Notes in Computer Science","volume":"1145","author":"Andersen P. H.","unstructured":"Andersen , P. H. and Holst , C. K . 1996. Termination analysis for offline partial evaluation of a higher order functional language . In Proceedings of the 3rd International Static Analysis Symposium (SAS), R. Cousot and D. A. Schmidt, Eds. Lecture Notes in Computer Science , vol. 1145 . Springer-Verlag, Berlin, Germany, 67--82.]] Andersen, P. H. and Holst, C. K. 1996. Termination analysis for offline partial evaluation of a higher order functional language. In Proceedings of the 3rd International Static Analysis Symposium (SAS), R. Cousot and D. A. Schmidt, Eds. Lecture Notes in Computer Science, vol. 1145. Springer-Verlag, Berlin, Germany, 67--82.]]"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings Rewriting Techniques and Applications RTA'97","volume":"1232","author":"Arts T.","unstructured":"Arts , T. and Giesl , J . 1997. Proving innermost termination automatically . In Proceedings Rewriting Techniques and Applications RTA'97 . Lecture Notes in Computer Science , vol. 1232 . Springer-Verlag, Berlin, Germany, 157--171.]] Arts, T. and Giesl, J. 1997. Proving innermost termination automatically. In Proceedings Rewriting Techniques and Applications RTA'97. Lecture Notes in Computer Science, vol. 1232. Springer-Verlag, Berlin, Germany, 157--171.]]"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/62678.62726"},{"volume-title":"The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, T. \u00c6","author":"Ben-Amram A. M.","key":"e_1_2_1_6_1","unstructured":"Ben-Amram , A. M. 2002. General size-change termination and lexicographic descent . In The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, T. \u00c6 . Mogensen, D. Schmidt, and I. H. Sudborough, Eds. Lecture Notes in Computer Science, vol. 2566 . Springer-Verlag , Berlin, Germany, 3--17.]] Ben-Amram, A. M. 2002. General size-change termination and lexicographic descent. In The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, T. \u00c6. Mogensen, D. Schmidt, and I. H. Sudborough, Eds. Lecture Notes in Computer Science, vol. 2566. Springer-Verlag, Berlin, Germany, 3--17.]]"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.62091"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/359863.359889"},{"volume-title":"Proceedings of the 6th International Symposium on Programming Language Implementation and Logic Programming (PLILP '94)","author":"Birkedal L.","key":"e_1_2_1_9_1","unstructured":"Birkedal , L. and Welinder , M . 1994. Hand-writing program generator generators . In Proceedings of the 6th International Symposium on Programming Language Implementation and Logic Programming (PLILP '94) , M. Hermenegildo and J. Penjam, Eds. Springer-Verlag, Berlin, Germany, 198--214.]] Birkedal, L. and Welinder, M. 1994. Hand-writing program generator generators. In Proceedings of the 6th International Symposium on Programming Language Implementation and Logic Programming (PLILP '94), M. Hermenegildo and J. Penjam, Eds. Springer-Verlag, Berlin, Germany, 198--214.]]"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90035-V"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90002-F"},{"key":"e_1_2_1_12_1","volume-title":"Tech. Rep. 93\/4, DIKU","author":"Bondorf A.","year":"1993","unstructured":"Bondorf , A. and J\u00f8rgensen , J . 1993 . Efficient analysis for realistic off-line partial evaluation: Extended version. Tech. Rep. 93\/4, DIKU , University of Copenhagen , Copenhagen, Denmark , Mar.]] Bondorf, A. and J\u00f8rgensen, J. 1993. Efficient analysis for realistic off-line partial evaluation: Extended version. Tech. Rep. 93\/4, DIKU, University of Copenhagen, Copenhagen, Denmark, Mar.]]"},{"key":"e_1_2_1_13_1","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis Symposium","author":"Brauburger J.","unstructured":"Brauburger , J. 1997. Automatic termination analysis for partial functions using polynomial orderings . In Static Analysis Symposium . Lecture Notes in Computer Science , vol. 1302 . Springer-Verlag , Berlin, Germany , 330--344.]] Brauburger, J. 1997. Automatic termination analysis for partial functions using polynomial orderings. In Static Analysis Symposium. Lecture Notes in Computer Science, vol. 1302. Springer-Verlag, Berlin, Germany, 330--344.]]"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321996"},{"key":"e_1_2_1_15_1","unstructured":"Cai J. Facon P. Henglein F. Paige R. and Schonberg E. 1991. Type analysis and data structure selection. In Constructing Programs from Specifications B. M\u00f6ller Ed. North-Holland Amsterdam The Netherlands 126--164.]] Cai J. Facon P. Henglein F. Paige R. and Schonberg E. 1991. Type analysis and data structure selection. In Constructing Programs from Specifications B. M\u00f6ller Ed. North-Holland Amsterdam The Netherlands 126--164.]]"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1012996816178"},{"key":"e_1_2_1_17_1","volume-title":"-W","author":"Chin W.-N.","year":"1998","unstructured":"Chin , W.-N. , Khoo , S.-C. , and Lee , T . -W . 1998 . Synchronisation analysis to stop tupling. In Programming Languages and Systems (ESOP'98) (Lisbon Portugal). Lecture Notes in Computer Science, vol. 1381 . Springer-Verlag , New York, 75--89.]] Chin, W.-N., Khoo, S.-C., and Lee, T.-W. 1998. Synchronisation analysis to stop tupling. In Programming Languages and Systems (ESOP'98) (Lisbon Portugal). Lecture Notes in Computer Science, vol. 1381. Springer-Verlag, New York, 75--89.]]"},{"key":"e_1_2_1_18_1","volume-title":"PSI'99","volume":"1755","author":"Christensen N. H.","unstructured":"Christensen , N. H. , Gl\u00fcck , R. , and Laursen , S . 2000. Binding-time analysis in partial evaluation: One size does Not fit all . In PSI'99 , D. Bj\u00f8rner, M. Broy, and A. Zamulin, Eds. Lecture Notes in Computer Science , vol. 1755 . Springer-Verlag, Berlin, Heidelberg, Germany, 80-- 92.]] Christensen, N. H., Gl\u00fcck, R., and Laursen, S. 2000. Binding-time analysis in partial evaluation: One size does Not fit all. In PSI'99, D. Bj\u00f8rner, M. Broy, and A. Zamulin, Eds. Lecture Notes in Computer Science, vol. 1755. Springer-Verlag, Berlin, Heidelberg, Germany, 80-- 92.]]"},{"key":"e_1_2_1_19_1","volume-title":"Conference on Computer-Aided Verification (CAV), E. Brinksma and K. G. Larsen, Eds. Lecture Notes in Computer Science","volume":"2404","author":"Col\u00f3n M. A.","unstructured":"Col\u00f3n , M. A. and Sipma , H. B . 2002. Practical methods for proving program termination . In Conference on Computer-Aided Verification (CAV), E. Brinksma and K. G. Larsen, Eds. Lecture Notes in Computer Science , vol. 2404 . Springer-Verlag, Berlin, Germany, 442--454.]] Col\u00f3n, M. A. and Sipma, H. B. 2002. Practical methods for proving program termination. In Conference on Computer-Aided Verification (CAV), E. Brinksma and K. G. Larsen, Eds. Lecture Notes in Computer Science, vol. 2404. Springer-Verlag, Berlin, Germany, 442--454.]]"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/154630.154645"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158707"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237767"},{"key":"e_1_2_1_23_1","unstructured":"Coquand C. 2001. The interactive theorem prover Agda. http:\/\/www.cs.chalmers.se\/~catarina\/agda\/.]] Coquand C. 2001. The interactive theorem prover Agda. http:\/\/www.cs.chalmers.se\/~catarina\/agda\/.]]"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_26_1","volume-title":"Eds","author":"Danvy O.","year":"1996","unstructured":"Danvy , O. , Gl\u00fcck , R. , and Thiemann , P. , Eds . 1996 . Partial Evaluation. Lecture Notes in Computer Science, vol. 1110 . Springer-Verlag , New York.]] Danvy, O., Gl\u00fcck, R., and Thiemann, P., Eds. 1996. Partial Evaluation. Lecture Notes in Computer Science, vol. 1110. Springer-Verlag, New York.]]"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/62678.62725"},{"key":"e_1_2_1_29_1","volume-title":"Tech. Rep. 1329, Computer Science Department","author":"Das M.","year":"1996","unstructured":"Das , M. and Reps , T . 1996 . BTA termination using CFL-reachability . Tech. Rep. 1329, Computer Science Department , University of Wisconsin-Madison.]] Das, M. and Reps, T. 1996. BTA termination using CFL-reachability. Tech. Rep. 1329, Computer Science Department, University of Wisconsin-Madison.]]"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(99)00030-8"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/800055.802050"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263706"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/800055.802051"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010095604496"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010043619517"},{"volume-title":"Proceedings of the 2nd Workshop on Meta-Programming in Logic","author":"Gallagher J.","key":"e_1_2_1_36_1","unstructured":"Gallagher , J. and Bruynooghe , M . 1990. Some low-level source transformations for logic programs . In Proceedings of the 2nd Workshop on Meta-Programming in Logic ( Leuven, Belgium, Apr.). M. Bruynooghe, Ed. Department of Computer Science, KU Leuven, Belgium, 229-- 246.]] Gallagher, J. and Bruynooghe, M. 1990. Some low-level source transformations for logic programs. In Proceedings of the 2nd Workshop on Meta-Programming in Logic (Leuven, Belgium, Apr.). M. Bruynooghe, Ed. Department of Computer Science, KU Leuven, Belgium, 229-- 246.]]"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/154630.154640"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507646"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237724"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/647163.717693"},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the 1998 DIKU International Summer School, J. Hatcliff, T. E. Mogenson, and P. Thiemann, Eds. Lecture Notes in Computer Science","volume":"1706","author":"Glenstrup A.","unstructured":"Glenstrup , A. , Makholm , H. , and Secher , J. P . 1999. C-Mix---Specialization of C programs. In Pratial Evaluation: Practice and Theory . Proceedings of the 1998 DIKU International Summer School, J. Hatcliff, T. E. Mogenson, and P. Thiemann, Eds. Lecture Notes in Computer Science , vol. 1706 . Springer-Verlag, New York, 108--154.]] Glenstrup, A., Makholm, H., and Secher, J. P. 1999. C-Mix---Specialization of C programs. In Pratial Evaluation: Practice and Theory. Proceedings of the 1998 DIKU International Summer School, J. Hatcliff, T. E. Mogenson, and P. Thiemann, Eds. Lecture Notes in Computer Science, vol. 1706. Springer-Verlag, New York, 108--154.]]"},{"key":"e_1_2_1_42_1","unstructured":"Glenstrup A. J. 1999. Terminator II: Stopping partial evaluation of fully recursive programs. M.S. thesis DIKU University of Copenhagen DK-2100 Copenhagen \u00f8.]] Glenstrup A. J. 1999. Terminator II: Stopping partial evaluation of fully recursive programs. M.S. thesis DIKU University of Copenhagen DK-2100 Copenhagen \u00f8.]]"},{"volume-title":"Perspectives of System Informatics: Proceedings of the Andrei Ershov Second International Memorial Conference. Lecture Notes in Computer Science. Springer-Verlag","author":"Glenstrup A. J.","key":"e_1_2_1_43_1","unstructured":"Glenstrup , A. J. and Jones , N. D . 1996. BTA algorithms to ensure termination of off-line partial evaluation . In Perspectives of System Informatics: Proceedings of the Andrei Ershov Second International Memorial Conference. Lecture Notes in Computer Science. Springer-Verlag , Berlin, Germany.]] Glenstrup, A. J. and Jones, N. D. 1996. BTA algorithms to ensure termination of off-line partial evaluation. In Perspectives of System Informatics: Proceedings of the Andrei Ershov Second International Memorial Conference. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany.]]"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Gl\u00fcck R. Nakashige R. and Z\u00f6chling R. 1995. Binding-time analysis applied to mathematical algorithms. In System Modelling and Optimization J. Dole\u017eal and J. Fidler Eds. Chapman & Hall London England 137--146.]] Gl\u00fcck R. Nakashige R. and Z\u00f6chling R. 1995. Binding-time analysis applied to mathematical algorithms. In System Modelling and Optimization J. Dole\u017eal and J. Fidler Eds. Chapman & Hall London England 137--146.]]","DOI":"10.1007\/978-0-387-34897-1_14"},{"key":"e_1_2_1_45_1","volume-title":"Eds. Lecture Notes in Computer Science","volume":"1110","author":"Gl\u00fcck R.","unstructured":"Gl\u00fcck , R. and S\u00f8rensen , M. H . 1996. A roadmap to metacomputation by supercompilation. In Partial Evaluation, O. Danvy, R. Gl\u00fcck, and P. Thiemann , Eds. Lecture Notes in Computer Science , vol. 1110 . Springer-Verlag, Berlin, Germany, 137--160.]] Gl\u00fcck, R. and S\u00f8rensen, M. H. 1996. A roadmap to metacomputation by supercompilation. In Partial Evaluation, O. Danvy, R. Gl\u00fcck, and P. Thiemann, Eds. Lecture Notes in Computer Science, vol. 1110. Springer-Verlag, Berlin, Germany, 137--160.]]"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00051-7"},{"key":"e_1_2_1_48_1","volume-title":"Eds","author":"Hatcliff J.","year":"1999","unstructured":"Hatcliff , J. , Mogensen , T. \u00c6., and Thiemann , P. , Eds . 1999 . Partial Evaluation : Practice and Theory. Proceedings of the 1998 DIKU International Summerschool. Lecture Notes in Computer Science, vol. 1706 . Springer-Verlag .]] Hatcliff, J., Mogensen, T. \u00c6., and Thiemann, P., Eds. 1999. Partial Evaluation: Practice and Theory. Proceedings of the 1998 DIKU International Summerschool. Lecture Notes in Computer Science, vol. 1706. Springer-Verlag.]]"},{"key":"e_1_2_1_50_1","series-title":"Lecture Notes in Computer Science","volume-title":"Finiteness analysis","author":"Holst C. K.","unstructured":"Holst , C. K. 1991. Finiteness analysis . In Functional Programming Languages and Computer Architecture, J. Hughes, Ed. Lecture Notes in Computer Science , vol. 523 . Springer-Verlag, Berlin , Germany , 473--495.]] Holst, C. K. 1991. Finiteness analysis. In Functional Programming Languages and Computer Architecture, J. Hughes, Ed. Lecture Notes in Computer Science, vol. 523. Springer-Verlag, Berlin, Germany, 473--495.]]"},{"volume-title":"Draft Proceedings, 4th Annual Glasgow Workshop on Functional Programming","author":"Holst C. K.","key":"e_1_2_1_51_1","unstructured":"Holst , C. K. and Launchbury , J . 1991. Handwriting cogen to avoid problems with static typing . In Draft Proceedings, 4th Annual Glasgow Workshop on Functional Programming . Glasgow University, Skye, Scotland, 210--218.]] Holst, C. K. and Launchbury, J. 1991. Handwriting cogen to avoid problems with static typing. In Draft Proceedings, 4th Annual Glasgow Workshop on Functional Programming. Glasgow University, Skye, Scotland, 210--218.]]"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/242224.242477"},{"volume-title":"Type specialisation for the \u03bb-calculus","author":"Hughes J.","key":"e_1_2_1_53_1","unstructured":"Hughes , J. 1996. Type specialisation for the \u03bb-calculus ; or a new paradigm for partial evaluation based on type inference. In Partial Evaluation, O. Danvy, R. Gl\u00fcck, and P. Thiemann, Eds. Lecture Notes in Computer Science, vol. 1110 . Springer-Verlag , New York, 183--215.]] Hughes, J. 1996. Type specialisation for the \u03bb-calculus; or a new paradigm for partial evaluation based on type inference. In Partial Evaluation, O. Danvy, R. Gl\u00fcck, and P. Thiemann, Eds. Lecture Notes in Computer Science, vol. 1110. Springer-Verlag, New York, 183--215.]]"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01806112"},{"volume-title":"International Seminar at Dagstuhl Castle","author":"Jones N. D.","key":"e_1_2_1_56_1","unstructured":"Jones , N. D. 1996. What Not to do when writing an interpreter for specialisation . In International Seminar at Dagstuhl Castle , Germany : Partial Evaluation, O. Danvy, R.Glck, and P. Thiemann, Eds. Lecture Notes in Computer Science, vol. 1110 . Springer-Verlag , Berlin, Germany, 216-- 237.]] Jones, N. D. 1996. What Not to do when writing an interpreter for specialisation. In International Seminar at Dagstuhl Castle, Germany: Partial Evaluation, O. Danvy, R.Glck, and P. Thiemann, Eds. Lecture Notes in Computer Science, vol. 1110. Springer-Verlag, Berlin, Germany, 216-- 237.]]"},{"key":"e_1_2_1_57_1","unstructured":"Jones N. D. Gomard C. K. and Sestoft P. 1993. Partial Evaluation and Automatic Program Generation. International Series in Computer Science. Prentice-Hall (New York). ISBN number 0-13-020249-5 (pbk).]] Jones N. D. Gomard C. K. and Sestoft P. 1993. Partial Evaluation and Automatic Program Generation. International Series in Computer Science. Prentice-Hall (New York). ISBN number 0-13-020249-5 (pbk).]]"},{"key":"e_1_2_1_58_1","doi-asserted-by":"crossref","unstructured":"Jones N. D. and Nielson F. 1994. Abstract interpretation: A semantics-based tool for program analysis. In Handbook of Logic in Computer Science. Oxford University Press New York. 527--629.]] Jones N. D. and Nielson F. 1994. Abstract interpretation: A semantics-based tool for program analysis. In Handbook of Logic in Computer Science. Oxford University Press New York. 527--629.]]","DOI":"10.1093\/oso\/9780198537809.003.0005"},{"volume-title":"Proceedings of the 18th International Conference in Software Engineering. IEEE Computer Society Press","author":"Kieburtz R. B.","key":"e_1_2_1_59_1","unstructured":"Kieburtz , R. B. , McKinney , L. , Bell , J. , Hook , J. , Kotov , A. , Lewis , J. , Oliva , D. , Sheard , T. , Smith , I. , and Walton , L . 1996. A software engineering experiment in software component generation . In Proceedings of the 18th International Conference in Software Engineering. IEEE Computer Society Press , Los Alamitos, CA, 542--553.]] Kieburtz, R. B., McKinney, L., Bell, J., Hook, J., Kotov, A., Lewis, J., Oliva, D., Sheard, T., Smith, I., and Walton, L. 1996. A software engineering experiment in software component generation. In Proceedings of the 18th International Conference in Software Engineering. IEEE Computer Society Press, Los Alamitos, CA, 542--553.]]"},{"volume-title":"Projection Factorisations in Partial Evaluation. Distinguished Dissertations in Computer Science","author":"Launchbury J.","key":"e_1_2_1_60_1","unstructured":"Launchbury , J. 1991. Projection Factorisations in Partial Evaluation. Distinguished Dissertations in Computer Science . Cambridge University Press , Cambridge .]] Launchbury, J. 1991. Projection Factorisations in Partial Evaluation. Distinguished Dissertations in Computer Science. Cambridge University Press, Cambridge.]]"},{"key":"e_1_2_1_61_1","volume-title":"Proceedings of the 3rd International Symposium on Theoretical Aspects of Computer Software (TACS'97)","volume":"1281","author":"Lawall J. L.","unstructured":"Lawall , J. L. and Thiemann , P . 1997. Sound specialization in the presence of computational effects . In Proceedings of the 3rd International Symposium on Theoretical Aspects of Computer Software (TACS'97) , M. Abadi and T. Ito, Eds. vol. 1281 . Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 165--190.]] Lawall, J. L. and Thiemann, P. 1997. Sound specialization in the presence of computational effects. In Proceedings of the 3rd International Symposium on Theoretical Aspects of Computer Software (TACS'97), M. Abadi and T. Ito, Eds. vol. 1281. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 165--190.]]"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.5555\/647171.718311"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_2_1_65_1","volume-title":"Proceedings","volume":"1503","author":"Leuschel M.","year":"1998","unstructured":"Leuschel , M. 1998 . On the power of homeomorphic embedding for online termination. In Static Analysis . Proceedings ( Pisa, Italy), G. Levi, Ed. Lecture Notes in Computer Science , vol. 1503 . Springer-Verlag, Berlin, 230--245.]] Leuschel, M. 1998. On the power of homeomorphic embedding for online termination. In Static Analysis. Proceedings (Pisa, Italy), G. Levi, Ed. Lecture Notes in Computer Science, vol. 1503. Springer-Verlag, Berlin, 230--245.]]"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1017\/S147106840200145X"},{"key":"e_1_2_1_67_1","doi-asserted-by":"crossref","unstructured":"Lindenstrauss N. and Sagiv Y. 1997. Automatic termination analysis of logic programs (with detailed experimental results). Unpublished. (http:\/\/www.cs.huji.ac.il\/~naomil\/.)]] Lindenstrauss N. and Sagiv Y. 1997. Automatic termination analysis of logic programs (with detailed experimental results). Unpublished. (http:\/\/www.cs.huji.ac.il\/~naomil\/.)]]","DOI":"10.7551\/mitpress\/4299.003.0011"},{"key":"e_1_2_1_68_1","volume-title":"Termilog: A system for checking termination of queries to logic programs. In Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22--25","author":"Lindenstrauss N.","year":"1997","unstructured":"Lindenstrauss , N. , Sagiv , Y. , and Serebrenik , A . 1997 . Termilog: A system for checking termination of queries to logic programs. In Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22--25 , O. Grumberg, Ed. Lecture Notes in Computer Science, vol. 1254 . Springer-Verlag , Berlin, Germany, 444--447.]] Lindenstrauss, N., Sagiv, Y., and Serebrenik, A. 1997. Termilog: A system for checking termination of queries to logic programs. In Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22--25, O. Grumberg, Ed. Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, Berlin, Germany, 444--447.]]"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026547031739"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(91)90027-M"},{"volume-title":"A basis for a mathematical theory of computation","author":"McCarthy J.","key":"e_1_2_1_71_1","unstructured":"McCarthy , J. 1964. A basis for a mathematical theory of computation . In Computer Programming and Formal Systems, P. Bradford and D. Hirschberg, Eds. North-Holland, Amsterdam , The Netherlands , 33--70.]] McCarthy, J. 1964. A basis for a mathematical theory of computation. In Computer Programming and Formal Systems, P. Bradford and D. Hirschberg, Eds. North-Holland, Amsterdam, The Netherlands, 33--70.]]"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/377769.377778"},{"volume-title":"Elsevier","author":"Mogensen T.","key":"e_1_2_1_73_1","unstructured":"Mogensen , T. \u00c6. 1988. Partially static structures in a self-applicable partial evaluator . In Partial Evaluation and Mixed Computation, D. Bj\u00f8rner, A. Ershov, and N. Jones, Eds. Elsevier Science Publishers , North- Holland, Amsterdam , The Netherlands. 325--347.]] Mogensen, T. \u00c6. 1988. Partially static structures in a self-applicable partial evaluator. In Partial Evaluation and Mixed Computation, D. Bj\u00f8rner, A. Ershov, and N. Jones, Eds. Elsevier Science Publishers, North-Holland, Amsterdam, The Netherlands. 325--347.]]"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026551132647"},{"key":"e_1_2_1_75_1","volume-title":"Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science","volume":"1576","author":"Moggi E.","unstructured":"Moggi , E. , Taha , W. , Benaissa , Z.-E.-A. , and Sheard , T . 1999. An idealized MetaML: Simpler, and more expressive . In Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science , vol. 1576 , Springer-Verlag, New York, 193--207.]] Moggi, E., Taha, W., Benaissa, Z.-E.-A., and Sheard, T. 1999. An idealized MetaML: Simpler, and more expressive. In Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science, vol. 1576, Springer-Verlag, New York, 193--207.]]"},{"key":"e_1_2_1_76_1","first-page":"144","article-title":"Operational semantics of termination types","volume":"3","author":"Nielson F.","year":"1996","unstructured":"Nielson , F. and Nielson , H. R. 1996 . Operational semantics of termination types . Nord. J. Comput. 3 , 144 -- 187 .]] Nielson, F. and Nielson, H. R. 1996. Operational semantics of termination types. Nord. J. Comput. 3, 144--187.]]","journal-title":"Nord. J. Comput."},{"key":"e_1_2_1_78_1","volume-title":"Academic Press","author":"P\u00e9ter R.","year":"1951","unstructured":"P\u00e9ter , R. 1951 . Rekursive Funktionen. Acad\u00e9miai Kiad\u00f3, Budapest, Hungary. (Translated and Printed as Recursive Function , Academic Press , New York , 1976).]] P\u00e9ter, R. 1951. Rekursive Funktionen. Acad\u00e9miai Kiad\u00f3, Budapest, Hungary. (Translated and Printed as Recursive Function, Academic Press, New York, 1976).]]"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/316686.316697"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/191839.191927"},{"key":"e_1_2_1_83_1","series-title":"Lecture Notes in Computer Science","volume-title":"Programs as Data Objects (PADO-II)","author":"Schultz U. P.","unstructured":"Schultz , U. P. 2001. Partial evaluation for class-based object-oriented languages . In Programs as Data Objects (PADO-II) . Lecture Notes in Computer Science , vol. 2053 . Springer-Verlag, Berlin , Germany , 173--197.]] Schultz, U. P. 2001. Partial evaluation for class-based object-oriented languages. In Programs as Data Objects (PADO-II). Lecture Notes in Computer Science, vol. 2053. Springer-Verlag, Berlin, Germany, 173--197.]]"},{"key":"e_1_2_1_85_1","volume-title":"Proceedings of the 3rd International School in Advanced Functional Programming (Braga, Portugal, Sept. 12--19","author":"Sheard T.","year":"1998","unstructured":"Sheard , T. 1999. Using MetaML: A staged programming language . In Proceedings of the 3rd International School in Advanced Functional Programming (Braga, Portugal, Sept. 12--19 , 1998 ), Revised Lectures, S. D. Swierstra, P. R. Henriques, and J. N. Oliveira, Eds. Lecture Notes in Computer Science vol, 1608, Springer-Verlag , New York, 207--239.]] Sheard, T. 1999. Using MetaML: A staged programming language. In Proceedings of the 3rd International School in Advanced Functional Programming (Braga, Portugal, Sept. 12--19, 1998), Revised Lectures, S. D. Swierstra, P. R. Henriques, and J. N. Oliveira, Eds. Lecture Notes in Computer Science vol, 1608, Springer-Verlag, New York, 207--239.]]"},{"key":"e_1_2_1_86_1","volume-title":"Ed. Lecture Notes in Computer Science","volume":"1924","author":"Song L.","unstructured":"Song , L. and Futamura , Y . 2000. A new termination approach for specialization. In Semantics, Applications, and Implementation of Program Generation, W. Taha , Ed. Lecture Notes in Computer Science , vol. 1924 . Springer-Verlag, Berlin, Germany, 72--91.]] Song, L. and Futamura, Y. 2000. A new termination approach for specialization. In Semantics, Applications, and Implementation of Program Generation, W. Taha, Ed. Lecture Notes in Computer Science, vol. 1924. Springer-Verlag, Berlin, Germany, 72--91.]]"},{"volume-title":"Logic Programming: Proceedings of the 1995 International Symposium, J. Lloyd, Ed. MIT Press","author":"S\u00f8rensen M. H.","key":"e_1_2_1_87_1","unstructured":"S\u00f8rensen , M. H. and Gl\u00fcck , R . 1995. An algorithm of generalization in positive supercompilation . In Logic Programming: Proceedings of the 1995 International Symposium, J. Lloyd, Ed. MIT Press , Cambridge, MA, 465--479.]] S\u00f8rensen, M. H. and Gl\u00fcck, R. 1995. An algorithm of generalization in positive supercompilation. In Logic Programming: Proceedings of the 1995 International Symposium, J. Lloyd, Ed. MIT Press, Cambridge, MA, 465--479.]]"},{"key":"e_1_2_1_88_1","volume-title":"Proceedings of the 4th International Symposium, SAS \u201997","volume":"1302","author":"Speirs C.","unstructured":"Speirs , C. , Somogyi , Z. , and S\u00f8ndergaard , H . 1997. Termination analysis for Mercury. In Static Analysis , Proceedings of the 4th International Symposium, SAS \u201997 ( Paris, France, Sept. 8--19), P. V. Hentenryck, Ed. Lecture Notes in Computer Science , vol. 1302 . Springer-Verlag, Berlin, Germany, 160--171.]] Speirs, C., Somogyi, Z., and S\u00f8ndergaard, H. 1997. Termination analysis for Mercury. In Static Analysis, Proceedings of the 4th International Symposium, SAS \u201997 (Paris, France, Sept. 8--19), P. V. Hentenryck, Ed. Lecture Notes in Computer Science, vol. 1302. Springer-Verlag, Berlin, Germany, 160--171.]]"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349219"},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/328691.328697"},{"key":"e_1_2_1_92_1","series-title":"Lecture Notes in Computer Science","volume-title":"Ont., Canada)","author":"Taha W.","unstructured":"Taha , W. , Ed. 2000. Semantics, Applications, and Implementation of Program Generation (Montreal , Ont., Canada) . Lecture Notes in Computer Science , vol. 1924 . Springer-Verlag , New York .]] Taha, W., Ed. 2000. Semantics, Applications, and Implementation of Program Generation (Montreal, Ont., Canada). Lecture Notes in Computer Science, vol. 1924. Springer-Verlag, New York.]]"},{"key":"e_1_2_1_93_1","volume-title":"Lecture Notes in Computer Science","volume":"2053","author":"Taha W.","unstructured":"Taha , W. , Makholm , H. , and Hughes , J . 2001. Tag elimination and Jones-optimality. In Programs as Data Objects (PADO-II) . Lecture Notes in Computer Science , vol. 2053 . Springer-Verlag, Berlin, 257--275. (http:\/\/cs-www.cs.yale.edu\/homes\/taha\/publications\/preprints\/pado00.dvi.)]] Taha, W., Makholm, H., and Hughes, J. 2001. Tag elimination and Jones-optimality. In Programs as Data Objects (PADO-II). Lecture Notes in Computer Science, vol. 2053. Springer-Verlag, Berlin, 257--275. (http:\/\/cs-www.cs.yale.edu\/homes\/taha\/publications\/preprints\/pado00.dvi.)]]"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00053-0"},{"volume-title":"TAPSOFT '97: Theory and Practice of Software Development (Lille, France)","author":"Thiemann P.","key":"e_1_2_1_95_1","unstructured":"Thiemann , P. 1997. A unified framework for binding-time analysis . In TAPSOFT '97: Theory and Practice of Software Development (Lille, France) . M. Bidoit and M. Dauchet, Eds. Lecture Notes in Computer Science, vol. 1214 . Springer-Verlag , Berlin, Germany, 742--756.]] Thiemann, P. 1997. A unified framework for binding-time analysis. In TAPSOFT '97: Theory and Practice of Software Development (Lille, France). M. Bidoit and M. Dauchet, Eds. Lecture Notes in Computer Science, vol. 1214. Springer-Verlag, Berlin, Germany, 742--756.]]"},{"volume-title":"Partial Evaluation: Practice and Theory. Proceedings of the 1998 DIKU International Summer School","author":"Thiemann P.","key":"e_1_2_1_96_1","unstructured":"Thiemann , P. 1999. Aspects of the PGG system: Specialization for standard scheme . In Partial Evaluation: Practice and Theory. Proceedings of the 1998 DIKU International Summer School . J. Hatcliff, T. E. Mogenson, and P. Thiemann, Eds. Lecture Notes in Computer Science, vol. 1706 . Springer-Verlag , New york, 412--432.]] Thiemann, P. 1999. Aspects of the PGG system: Specialization for standard scheme. In Partial Evaluation: Practice and Theory. Proceedings of the 1998 DIKU International Summer School. J. Hatcliff, T. E. Mogenson, and P. Thiemann, Eds. Lecture Notes in Computer Science, vol. 1706. Springer-Verlag, New york, 412--432.]]"},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1145\/954063.954069"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.5555\/645387.651542"},{"key":"e_1_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319871"},{"key":"e_1_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019916231463"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1108970.1108973","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1108970.1108973","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:07:50Z","timestamp":1750262870000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1108970.1108973"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,11]]},"references-count":93,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2005,11]]}},"alternative-id":["10.1145\/1108970.1108973"],"URL":"https:\/\/doi.org\/10.1145\/1108970.1108973","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2005,11]]},"assertion":[{"value":"2005-11-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}