{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T05:39:37Z","timestamp":1737005977840,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":78,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540442844"},{"type":"electronic","value":"9783540458210"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45821-2_1","type":"book-chapter","created":{"date-parts":[[2007,5,3]],"date-time":"2007-05-03T16:58:47Z","timestamp":1178211527000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Program Generation, Termination, and Binding-Time Analysis"],"prefix":"10.1007","author":[{"given":"Neil D.","family":"Jones","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arne J.","family":"Glenstrup","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,26]]},"reference":[{"key":"1_CR1","unstructured":"Andreas Abel and Thorsten Altenkirch. A semantical analysis of structural recursion. In Abstracts of the Fourth International Workshop on Termination WST\u201999, pages 24\u201325. unpublished, May 1999."},{"key":"1_CR2","unstructured":"Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools. Addison Wesley, 1986."},{"key":"1_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/3-540-62950-5_68","volume-title":"Proceedings Rewriting Techniques and Applications RTA\u201997","author":"T. Arts","year":"1997","unstructured":"Thomas Arts and J\u00fcrgen Giesl. Proving innermost termination automatically. In Proceedings Rewriting Techniques and Applications RTA\u201997, volume 1232 of Lecture Notes in Computer Science, pages 157\u2013171. Springer, 1997."},{"issue":"12","key":"1_CR4","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/2.62091","volume":"23","author":"A. Berlin","year":"1990","unstructured":"Andrew Berlin and Daniel Weise. Compiling scientific code using partial evaluation. IEEE Computer, 23(12):25\u201337, 1990.","journal-title":"IEEE Computer"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Lars Birkedal and Morten Welinder. Hand-writing program generator generators. In M. Hermenegildo and J. Penjam, editors, Proceedings of the 6th International Symposium on Programming Language Implementation and Logic Programming (PLILP\u2019 94), pages 198\u2013214. Springer-Verlag, September 1994.","DOI":"10.1007\/3-540-58402-1_15"},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0167-6423(91)90035-V","volume":"17","author":"A. Bondorf","year":"1991","unstructured":"Anders Bondorf. Automatic autoprojection of higher order recursive equations. Science of Computer Programming, 17:3\u201334, 1991.","journal-title":"Science of Computer Programming"},{"key":"1_CR7","volume-title":"Technical Report 93\/4","author":"A. Bondorf","year":"1993","unstructured":"Anders Bondorf and Jesper J\u00f8rgensen. Efficient analyses for realistic off-line partial evaluation: extended version. Technical Report 93\/4, DIKU, University of Copenhagen, Denmark, 1993."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Rod M. Burstall and John Darlington. A transformation system for developing recursive programs. Journal of the ACM, 24(1):44\u201367, January 1977.","DOI":"10.1145\/321992.321996"},{"key":"1_CR9","unstructured":"Jiazhen Cai, P. Facon, Fritz Henglein, Robert Paige, and Edmond Schonberg. Type analysis and data structure selection. In Constructing Programs From Specifications, pages 325\u2013347. North-Holland, 1991."},{"issue":"2\/3","key":"1_CR10","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1023\/A:1012996816178","volume":"14","author":"W.-N. Chin","year":"2002","unstructured":"Wei-Ngan Chin and Siau-Cheng Khoo. Calculating sized types. Higher-Order and Symbolic Computation, 14(2\/3):261\u2013300, 2002.","journal-title":"Higher-Order and Symbolic Computation"},{"key":"1_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/BFb0053564","volume-title":"Programming Languages and Systems (ESOP\u201998)","author":"W.-N. Chin","year":"1998","unstructured":"Wei-Ngan Chin, Siau-Cheng Khoo, and Tat-Wee Lee. Synchronisation analysis to stop tupling. In Programming Languages and Systems (ESOP\u201998), pages 75\u201389, Lisbon, 1998. Springer LNCS 1381."},{"key":"1_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/3-540-46562-6_7","volume-title":"Perspectives of System Informatics. Proceedings","author":"N. H. Christensen","year":"2000","unstructured":"Niels H. Christensen, Robert Gl\u00fcck, and S\u00f8ren Laursen. Binding-time analysis in partial evaluation: One size does not fit all. In D. Bj\u00f8rner, M. Broy, and A. V. Zamulin, editors, Perspectives of System Informatics. Proceedings, volume 1755 of Lecture Notes in Computer Science, pages 80\u201392. Springer-Verlag, 2000."},{"key":"1_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Conference on Computer-Aided Verification (CAV)","author":"M. A. Col\u00f3n","year":"2002","unstructured":"Michael A. Col\u00f3n and Henny B. Sipma. Practical methods for proving program termination. In Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science, pages ??-?? Springer-Verlag, 2002."},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Charles Consel. A tour of Schism: a partial evaluation system for higher-order applicative languages. In ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 66\u201377, 1993.","DOI":"10.1145\/154630.154645"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In ACM Symposium on Principles of Programming Languages, pages 493\u2013501. ACM Press, 1993.","DOI":"10.1145\/158511.158707"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Charles Consel and Fran\u00e7ois No\u00ebl. A general approach for run-time specialization and its application to C. In ACM Symposium on Principles of Programming Languages, pages 145\u2013156, 1996.","DOI":"10.1145\/237721.237767"},{"key":"1_CR17","unstructured":"Catarina Coquand. The interactive theorem prover Agda. http:\/\/www.cs.chalmers.se\/~catarina\/agda\/ , 2001."},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn Laubach, and Hongjun Zheng. Bandera: Extracting finite-state models from Java source code. In 22nd International Conference on Software Engineering, pages 439\u2013448. IEEE Press, 2000.","DOI":"10.1145\/337180.337234"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In 4th POPL, Los Angeles, CA, pages 238\u2013252, Jan. 1977.","DOI":"10.1145\/512950.512973"},{"key":"1_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Partial Evaluation","year":"1996","unstructured":"Olivier Danvy, Robert Gl\u00fcck, and Peter Thiemann, editors. Partial Evaluation, volume 1110 of Lecture Notes in Computer Science. Springer-Verlag, 1996."},{"key":"1_CR21","unstructured":"Manuvir Das. Partial Evaluation using Dependence Graphs. PhD thesis, University of Wisconsin-Madison, February 1998."},{"key":"1_CR22","unstructured":"Manuvir Das and Thomas Reps. BTA termination using CFL-reachability. Technical Report 1329, Computer Science Department, University of Wisconsin-Madison, 1996."},{"issue":"4","key":"1_CR23","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1023\/A:1010095604496","volume":"12","author":"Y. Futamura","year":"1999","unstructured":"Yoshihiko Futamura. Partial evaluation of computation process-an approach to a compiler-compiler. Higher-Order and Symbolic Computation, 12(4):381\u2013391, 1999. Reprinted from Systems \u00b7 Computers \u00b7 Controls 2(5), 1971.","journal-title":"Higher-Order and Symbolic Computation"},{"issue":"4","key":"1_CR24","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1023\/A:1010043619517","volume":"12","author":"Y. Futamura","year":"1999","unstructured":"Yoshihiko Futamura. Partial evaluation of computation process, revisited. Higher-Order and Symbolic Computation, 12(4):377\u2013380, 1999.","journal-title":"Higher-Order and Symbolic Computation"},{"key":"1_CR25","first-page":"229","volume-title":"Proceedings of the Second Workshop on Meta-Programming in Logic, April 1990, Leuven, Belgium","author":"J. Gallagher","year":"1990","unstructured":"John Gallagher and Maurice Bruynooghe. Some low-level source transformations for logic programs. In M. Bruynooghe, editor, Proceedings of the Second Workshop on Meta-Programming in Logic, April 1990, Leuven, Belgium, pages 229\u2013246. Department of Computer Science, KU Leuven, Belgium, 1990."},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"John P. Gallagher. Tutorial on specialisation of logic programs. In Proceedings of PEPM\u201993, the ACM Sigplan Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 88\u201398. ACM Press, 1993.","DOI":"10.1145\/154630.154640"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Steve Ganz, Amr Sabry, and Walid Taha. Macros as Multi-Stage computations: Type-Safe, generative, binding macros in MacroML. In Cindy Norris and Jr. James B. Fenwick, editors, Proceedings of the Sith ACM SIGPLAN International Conference on Functional Programming (ICFP-01), volume 36, 10 of ACM SIGPLAN notices, pages 74\u201385, New York, September 3\u20135 2001. ACM Press.","DOI":"10.1145\/507669.507646"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Arne Glenstrup, Henning Makholm, and Jens Peter Secher. C-Mix \u2014specialization of C programs. In Torben Mogensen, and Peter Thiemann, editors. Partial Evaluation: Practice and Theory. Proceedings of the 1998 DIKU International Summerschool, volume 1706. Springer-Verlag, 1999. Hatcliff et al. [35], pages 108\u2013154.","DOI":"10.1007\/3-540-47018-2_4"},{"key":"1_CR29","unstructured":"Arne John Glenstrup. Terminator II: Stopping partial evaluation of fully recursive programs. Master\u2019s thesis, DIKU, University of Copenhagen, Universitetsparken 1, DK-2100 Copenhagen \u00d8, June 1999."},{"key":"1_CR30","unstructured":"Arne John Glenstrup. Partial evaluation, termination analysis, and specialisation-point insertion. In preparation, 2002."},{"key":"1_CR31","series-title":"Lect Notes Comput Sci","volume-title":"Perspectives of System Informatics: Proceedings of the Andrei Ershov Second International Memorial Conference","author":"A. J. Glenstrup","year":"1996","unstructured":"Arne John Glenstrup and Neil D. Jones. 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, June 1996."},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Robert Gl\u00fcck, Ryo Nakashige, and Robert Z\u00f6chling. Binding-time analysis applied to mathematical algorithms. In J. Dole\u017eal and J. Fidler, editors, System Modelling and Optimization, pages 137\u2013146. Chapman & Hall, 1995.","DOI":"10.1007\/978-0-387-34897-1_14"},{"key":"1_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-61580-6_8","volume-title":"Partial Evaluation","author":"R. Gl\u00fcck","year":"1996","unstructured":"Robert Gl\u00fcck and Morten Heine S\u00f8rensen. A roadmap to metacomputation by supercompilation. In O. Danvy, R. Gl\u00fcck, and P. Thiemann, editors, Partial Evaluation, volume 1110 of Lecture Notes in Computer Science, pages 137\u2013160. Springer-Verlag, 1996."},{"issue":"1\u20132","key":"1_CR34","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0304-3975(00)00051-7","volume":"248","author":"B. Grant","year":"2000","unstructured":"Brian Grant, Markus Mock, Matthai Philipose, Craig Chambers, and Susan J. Eggers. DyC: An expressive annotation-directed dynamic compiler for C. Theoretical Computer Science, 248(1\u20132):147\u2013199, 2000.","journal-title":"Theoretical Computer Science"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"John Hatcliff, Torben Mogensen, and Peter Thiemann, editors. Partial Evaluation: Practice and Theory. Proceedings of the 1998 DIKU International Summerschool, volume 1706. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-47018-2"},{"key":"1_CR36","unstructured":"Carsten Kehler Holst and John Launchbury. Handwriting cogen to avoid problems with static typing. In Draft Proceedings, Fourth Annual Glasgow Workshop on Functional Programming, Skye, Scotland, pages 210\u2013218. Glasgow University, 1991."},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Paul Hudak. Building domain specific embedded languages. ACM Computing Surveys, 28A:(electronic), December 1996.","DOI":"10.1145\/242224.242477"},{"key":"1_CR38","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/3-540-61580-6_10","volume-title":"Partial Evaluation","author":"J. Hughes","year":"1996","unstructured":"John Hughes. Type specialisation for the \u03bb-calculus; or a new paradigm for partial evaluation based on type inference. In Robert Gl\u00fcck, and Peter Thiemann, editors. Partial Evaluation, volume 1110 of Lecture Notes in Computer Science. Springer-Verlag, 1996.Danvy et al. [20], pages 183\u2013215."},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"John Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems using sized types. In Olivier Danvy, Robert Gl\u00fcck, and Peter Thiemann, editors, ACM Symposium on Principles of Programming Languages, pages 410\u2013423. ACM Press, 1996.","DOI":"10.1145\/237721.240882"},{"key":"1_CR40","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/3-540-61580-6_11","volume-title":"Partial Evaluation","author":"N. D. Jones","year":"1996","unstructured":"Neil D. Jones. What Not to do when writing an interpreter for specialisation. In Robert Gl\u00fcck, and Peter Thiemann, editors. Partial Evaluation, volume 1110 of Lecture Notes in Computer Science. Springer-Verlag, 1996.Danvy et al. [20], pages 216\u2013237."},{"key":"1_CR41","unstructured":"Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall. Download accessible from http:\/\/www.diku.dk\/users\/neil , 1993."},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Neil D. Jones and Flemming Nielson. Abstract interpretation: a semantics-based tool for program analysis. In Handbook of Logic in Computer Science. Oxford University Press, 1994. 527\u2013629.","DOI":"10.1093\/oso\/9780198537809.003.0005"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Richard B. Kieburtz, Laura McKinney, Jeffrey Bell, James Hook, Alex Kotov, Jeffrey Lewis, Dino Oliva, Tim Sheard, Ira Smith, and Lisa Walton. A software engineering experiment in software component generation. In 18th International Conference in Software Engineering, pages 542\u2013553, 1996.","DOI":"10.1109\/ICSE.1996.493448"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"John Launchbury. Projection Factorisations in Partial Evaluation. Distinguished Dissertations in Computer Science. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569814"},{"key":"1_CR45","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/BFb0014551","volume-title":"Proceedings of the 3rd International Symposium on Theoretical Aspects of Computer Software (TACS\u201997)","author":"J. L. Lawall","year":"1997","unstructured":"Julia L. Lawall and Peter Thiemann. Sound specialization in the presence of computational effects. In M. Abadi and T. Ito, editors, Proceedings of the 3rd International Symposium on Theoretical Aspects of Computer Software (TACS\u201997), number 1281 in Lecture Notes in Computer Science, pages 165\u2013190, September 1997."},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In ACM Symposium on Principles of Programming Languages, volume 28, pages 81\u201392. ACM Press, January 2001.","DOI":"10.1145\/373243.360210"},{"key":"1_CR47","doi-asserted-by":"crossref","unstructured":"Michael Leuschel. On the power of homeomorphic embedding for online termination. In Static Analysis. Proceedings, volume 1503, pages 230\u2013245. Springer-Verlag, September 1998.","DOI":"10.1007\/3-540-49727-7_14"},{"key":"1_CR48","doi-asserted-by":"crossref","unstructured":"Michael Leuschel and Maurice Bruynooghe. Logic program specialisation through partial deduction: Control issues. Theory and Practice of Logic Programming, 2002.","DOI":"10.1017\/S147106840200145X"},{"key":"1_CR49","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"444","DOI":"10.1007\/3-540-63166-6_44","volume-title":"Computer Aided Verification, 9th International Conference, CAV\u2019 97, Haifa, Israel, Jun 22\u201325, 1997","author":"N. Lindenstrauss","year":"1997","unstructured":"Naomi Lindenstrauss, Yehoshua Sagiv, and Alexander Serebrenik. Termilog: A system for checking termination of queries to logic programs. In Orna Grumberg, editor, Computer Aided Verification, 9th International Conference, CAV\u2019 97, Haifa, Israel, Jun 22\u201325, 1997, volume 1254 of Lecture Notes in Computer Science, pages 444\u2013447. Springer, 1997."},{"issue":"4","key":"1_CR50","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1023\/A:1026547031739","volume":"13","author":"Y. Liu","year":"2000","unstructured":"Y.\u00c3. Liu. Efficiency by incrementalization: an introduction. Journal of Higher-Order and Symbolic Computation, 13(4):289\u2013313, 2000.","journal-title":"Journal of Higher-Order and Symbolic Computation"},{"key":"1_CR51","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0743-1066(91)90027-M","volume":"11","author":"J. W. Lloyd","year":"1991","unstructured":"John W. Lloyd and John C. Shepherdson. Partial evaluation in logic programming. Journal of Logic Programming, 11:217\u2013242, 1991.","journal-title":"Journal of Logic Programming"},{"issue":"2","key":"1_CR52","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/377769.377778","volume":"19","author":"M. Dylan","year":"2001","unstructured":"Dylan McNamee, Jonathan Walpole, Calton Pu, Crispin Cowan, Charles Krasic, Ashvin Goel, Perry Wagle, Charles Consel, Gilles Muller, and Renaud Marlet. Specialization tools and techniques for systematic optimization of system software. A CM Transactions on Computer Systems, 19(2):217\u2013251, 2001.","journal-title":"A CM Transactions on Computer Systems"},{"key":"1_CR53","unstructured":"Torben Mogensen. Partially static structures in a self-applicable partial evaluator. In D. Bj\u00f8rner, A.P. Ershov, and N.D. Jones, editors, Partial Evaluation and Mixed Computation, pages 325\u2013347. North-Holland, 1988."},{"key":"1_CR54","first-page":"193","volume":"1576","author":"E. Moggi","year":"1999","unstructured":"Eugenio Moggi, Walid Taha, Zine-El-Abidine Benaissa, and Tim Sheard. An idealized MetaML: Simpler, and more expressive. In European Symposium on Programming, volume 1576, pages 193\u2013207, 1999.","journal-title":"European Symposium on Programming"},{"key":"1_CR55","unstructured":"Oregon Graduate Institute Technical Reports. P.O. Box 91000, Portland, OR 97291-1000, USA. Available online from ftp:\/\/cse.ogi.edu\/pub\/tech-reports\/README.html ."},{"key":"1_CR56","volume-title":"Rekursive Funktionen (Recursive Functions)","author":"R. P\u00e9ter","year":"1951","unstructured":"Rosza P\u00e9ter. Rekursive Funktionen (Recursive Functions). Acad\u00e9miai Kiad\u00f3, Budapest (Academic Press, New York), 1951 (1976)."},{"key":"1_CR57","doi-asserted-by":"crossref","unstructured":"Massimiliano Poletto, Wilson C. Hsieh, Dawson R. Engler, and M. Frans Kaashoek. \u2018C and tcc: A language and compiler for dynamic code generation. ACM Transactions on Programming Languages and Systems, 21(2):324\u2013369, March 1999.","DOI":"10.1145\/316686.316697"},{"key":"1_CR58","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A. P. Sistla","year":"1987","unstructured":"Aravinda Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation problem for B\u00fcchi automata with applications to temporal logic. Theoretical Computer Science, 49:217\u2013237, 1987.","journal-title":"Theoretical Computer Science"},{"key":"1_CR59","doi-asserted-by":"crossref","unstructured":"Konstantinos F. Sagonas, Terrance Swift, and David Scott Warren. XSB as an efficient deductive database engine. In Richard T. Snodgrass and Marianne Winslett, editors, Proceedings of the 1994 ACM SIGMOD International Conference on Management of Data, Minneapolis, Minnesota, May 24\u201327, 1994, pages 442\u2013453. ACM Press, 1994.","DOI":"10.1145\/191843.191927"},{"issue":"2&3","key":"1_CR60","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/S0743-1066(99)00030-8","volume":"41","author":"D. Schreye De","year":"1999","unstructured":"Danny De Schreye, Robert Gl\u00fcck, Jesper J\u00f8rgensen, Michael Leuschel, Bern Martens, and Morten H. B. S\u00f8rensen. Conjunctive partial deduction: Foundations, control, algorithms, and experiments. Journal of Logic Programming, 41(2&3):231\u2013277, 1999.","journal-title":"Journal of Logic Programming"},{"key":"1_CR61","doi-asserted-by":"crossref","unstructured":"Ulrik Schultz. Partial evaluation for class-based object-oriented languages. In PADO, pages 173\u2013197, 2001.","DOI":"10.1007\/3-540-44978-7_11"},{"key":"1_CR62","unstructured":"Peter Sestoft. Bibliography on partial evaluation and mixed computation (bibtex format, online ftp:\/\/ftp.diku.dk\/diku\/semantics\/partial-evaluation\/ ). Technical report, DIKU (Computer Science, University of Copenhagen), 2001."},{"key":"1_CR63","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/10704973_5","volume-title":"Advanced Functional Programming","author":"T. Sheard","year":"1999","unstructured":"Tim Sheard. Using MetaML: A staged programming language. Lecture Notes in Computer Science, 1608:207--??, 1999."},{"key":"1_CR64","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-45350-4_8","volume-title":"Semantics, Applications, and Implementation of Program Generation","author":"L. Song","year":"2000","unstructured":"Litong Song and Yoshihiko Futamura. A new termination approach for specialization. In [70], pages 72\u201391, 2000."},{"key":"1_CR65","unstructured":"Morten Heine S\u00f8rensen and Robert Gl\u00fcck. An algorithm of generalization in positive supercompilation. In J.W. Lloyd, editor, Logic Programming: Proceedings of the 1995 International Symposium, pages 465\u2013479. MIT Press, 1995."},{"key":"1_CR66","series-title":"Lect Notes Comput Sci","first-page":"160","volume-title":"Static Analysis, Proceedings of the 4th International Symposium, SAS\u2019 97, Paris, France, Sep 8\u201319, 1997","author":"C. Speirs","year":"1997","unstructured":"Chris Speirs, Zoltan Somogyi, and Harald S\u00f8ndergaard. Termination analysis for Mercury. In Pascal Van Hentenryck, editor, Static Analysis, Proceedings of the 4th International Symposium, SAS\u2019 97, Paris, France, Sep 8\u201319, 1997, volume 1302 of Lecture Notes in Computer Science, pages 160\u2013171. Springer, 1997."},{"issue":"2","key":"1_CR67","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1145\/349214.349219","volume":"22","author":"Michael Sperber","year":"2000","unstructured":"Michael Sperber and Peter Thiemann. Generation of LR parsers by partial evaluation. ACM Transactions on Programming Languages and Systems, 22(2):224\u2013264, March 2000.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR68","doi-asserted-by":"crossref","unstructured":"Walid Taha. A sound reduction semantics for untyped CBN multi-stage computation. or, the theory of MetaML is non-trival. ACM SIGPLAN Notices, 34(11):34\u201343, November 1999. Extended abstract.","DOI":"10.1145\/328691.328697"},{"key":"1_CR69","unstructured":"Walid Taha. Multi-Stage Programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology, 1999. Available from [55]."},{"key":"1_CR70","series-title":"Lect Notes Comput Sci","volume-title":"Semantics, Applications, and Implementation of Program Generation","year":"2000","unstructured":"Walid Taha, editor. Semantics, Applications, and Implementation of Program Generation, volume 1924 of Lecture Notes in Computer Science, Montr\u00e9al, 2000. Springer-Verlag."},{"key":"1_CR71","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/3-540-45449-7_13","volume-title":"the International Workshop on Embedded Software (ES\u2019 01)","author":"W. Taha","year":"2001","unstructured":"Walid Taha, Paul Hudak, and Zhanyong Wan. Directions in functional program-ming for real(-time) applications. In the International Workshop on Embedded Software (ES\u2019 01), volume 221 of Lecture Notes in Computer Science, pages 185\u2013203, Lake Tahoe, 2001. Springer-Verlag."},{"key":"1_CR72","doi-asserted-by":"crossref","unstructured":"Walid Taha, Henning Makholm, and John Hughes. Tag elimination and Jones-optimality. In PADO, pages 257\u2013275, 2001. http:\/\/cs-www.cs.yale.edu\/homes\/taha\/publications\/preprints\/pado00.dvi .","DOI":"10.1007\/3-540-44978-7_15"},{"issue":"1\u20132","key":"1_CR73","first-page":"211","volume":"248","author":"Walid Taha and Tim Sheard","year":"2000","unstructured":"Walid Taha and Tim Sheard. MetaML and multi-stage programming with explicit annotations. Theoretical Computer Science, 248(1\u20132):211\u2013242, October 2000.","journal-title":"Theoretical Computer Science"},{"key":"1_CR74","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"742","DOI":"10.1007\/BFb0030638","volume-title":"TAPSOFT\u2019 97: Theory and Practice of Software Development, Lille, France, April 1997","author":"P. Thiemann","year":"1997","unstructured":"Peter Thiemann. A unified framework for binding-time analysis. In M. Bidoit and M. Dauchet, editors, TAPSOFT\u2019 97: Theory and Practice of Software Development, Lille, France, April 1997. (Lecture Notes in Computer Science, vol. 1214), pages 742\u2013756. Springer-Verlag, 19"},{"key":"1_CR75","unstructured":"Peter Thiemann. Aspects of the pgg system: Specialization for standard scheme. In Hatcliff et al. Torben Mogensen, and Peter Thiemann, editors. Partial Evaluation: Practice and Theory. Proceedings of the 1998 DIKU International Summerschool, volume 1706. Springer-Verlag, 1999. [35], pages 412\u2013432."},{"key":"1_CR76","doi-asserted-by":"crossref","unstructured":"Valentin F. Turchin. A supercompiler system based on the language Refal. SIGPLAN Notices, 14(2):46\u201354, February 1979.","DOI":"10.1145\/954063.954069"},{"key":"1_CR77","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"344","DOI":"10.1007\/3-540-19027-9_23","volume-title":"ESOP\u201988. 2nd European Symposium on Programming, Nancy, France, March 1988","author":"P. Wadler","year":"1988","unstructured":"Philip Wadler. Deforestation: Transforming programs to eliminate trees. In H. Ganzinger, editor, ESOP\u201988. 2nd European Symposium on Programming, Nancy, France, March 1988. (Lecture Notes in Computer Science, vol. 300), pages 344\u2013358. Springer-Verlag, 19"},{"key":"1_CR78","first-page":"91","volume":"15","author":"H. Xi","year":"2002","unstructured":"Hongwei Xi. Dependent types for program termination verification. volume 15, pages 91\u2013132, 2002.","journal-title":"Dependent types for program termination verification"}],"container-title":["Lecture Notes in Computer Science","Generative Programming and Component Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45821-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T00:49:21Z","timestamp":1736988561000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45821-2_1"}},"subtitle":["Invited Paper"],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540442844","9783540458210"],"references-count":78,"URL":"https:\/\/doi.org\/10.1007\/3-540-45821-2_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"26 September 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}