Termination analysis and specialization-point insertion in offline partial evaluation

ABSTRACT

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 necessary, 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 termination 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 “generating extensions,” the program generators that most offline partial evaluators produce.The technique is based on size-change graphs that approximate the changes in parameter sizes at function calls. We formulate a criterion, bounded anchoring, for detecting parameters known to be bounded during specialization: a bounded parameter can act as an anchor 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 guarantees 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.

REFERENCES

• 1: 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.
• 2: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 3: Peter Holst Andersen , Carsten Kehler Holst, Termination Analysis for Offline Partial Evaluation of a Higher Order Functional Language, Proceedings of the Third International Symposium on Static Analysis, p.67-82, September 24-26, 1996
• 4: Thomas Arts , Jürgen Giesl, Proving Innermost Normalisation Automatically, Proceedings of the 8th International Conference on Rewriting Techniques and Applications, p.157-171, June 02-05, 1997
• 5: Alan Bawden, Reification without evaluation, Proceedings of the 1988 ACM conference on LISP and functional programming, p.342-349, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62726]
• 6: Amir M. Ben-Amram, General size-change termination and lexicographic descent, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
• 7: Andrew Berlin , Daniel Weise, Compiling Scientific Code Using Partial Evaluation, Computer, v.23 n.12, p.25-37, December 1990 [doi>10.1109/2.62091]
• 8: R. S. Bird, Improving programs by the introduction of recursion, Communications of the ACM, v.20 n.11, p.856-863, Nov. 1977 [doi>10.1145/359863.359889]
• 9: Lars Birkedal , Morten Welinder, Hand-Writing Program Generator Generators, Proceedings of the 6th International Symposium on Programming Language Implementation and Logic Programming, p.198-214, September 14-16, 1994
• 10: Anders Bondorf, Automatic autoprojection of higher order recursive equations, Science of Computer Programming, v.17 n.1-3, p.3-34, Dec. 1991
• 11: Anders Bondorf , Olivier Danvy, Automatic autoprojection of recursive equations with global variable and abstract data types, Science of Computer Programming, v.16 n.2, p.151-195, Sept. 1991 [doi>10.1016/0167-6423(91)90002-F]
• 12: Bondorf, A. and Jørgensen, J. 1993. Efficient analysis for realistic off-line partial evaluation: Extended version. Tech. Rep. 93/4, DIKU, University of Copenhagen, Copenhagen, Denmark, Mar.
• 13: Jürgen Brauburger, Automatic Termination Analysis for Partial Functions Using Polynomial Orderings, Proceedings of the 4th International Symposium on Static Analysis, p.330-344, September 08-10, 1997
• 14: R. M. Burstall , John Darlington, A Transformation System for Developing Recursive Programs, Journal of the ACM (JACM), v.24 n.1, p.44-67, Jan. 1977 [doi>10.1145/321992.321996]
• 15: 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öller, Ed. North-Holland, Amsterdam, The Netherlands, 126--164.
• 16: Wei-Ngan Chin , Siau-Cheng Khoo, Calculating Sized Types, Higher-Order and Symbolic Computation, v.14 n.2-3, p.261-300, September 2001 [doi>10.1023/A:1012996816178]
• 17: Wei-Ngan Chin , Siau-Cheng Khoo , Tat-Wee Lee, Synchronisation Analysis to Stop Tulping, Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems, p.75-89, March 28-April 04, 1998
• 18: Niels H. Christensen , Robert Glück , Søren Laursen, Binding-Time Analysis in Partial Evaluation: One Size Does Not Fit All, Proceedings of the Third International Andrei Ershov Memorial Conference on Perspectives of System Informatics, p.80-92, July 06-09, 1999
• 19: Michael Colón , Henny Sipma, Practical Methods for Proving Program Termination, Proceedings of the 14th International Conference on Computer Aided Verification, p.442-454, July 27-31, 2002
• 20: Charles Consel, A tour of Schism: a partial evaluation system for higher-order applicative languages, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.145-154, June 14-16, 1993, Copenhagen, Denmark [doi>10.1145/154630.154645]
• 21: Charles Consel , Olivier Danvy, Tutorial notes on partial evaluation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.493-501, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158707]
• 22: Charles Consel , François Noël, A general approach for run-time specialization and its application to C, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.145-156, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237767]
• 23: Coquand, C. 2001. The interactive theorem prover Agda. http://www.cs.chalmers.se/~catarina/agda/.
• 24: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 25: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 26: Selected Papers from the Internaltional Seminar on Partial Evaluation, February 1996
• 27: Olivier Danvy , Karoline Malmkjaer, Intensions and extensions in a reflective tower, Proceedings of the 1988 ACM conference on LISP and functional programming, p.327-341, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62725]
• 28: Manuvir Das , Thomas W. Reps, Partial evaluation using dependence graphs, 1998
• 29: Das, M. and Reps, T. 1996. BTA termination using CFL-reachability. Tech. Rep. 1329, Computer Science Department, University of Wisconsin-Madison.
• 30: De Schreye, D., Glück, R., Jørgensen, J., Leuschel, M., Martens, B., and Sørensen, M. H. B. 1999. Conjunctive partial deduction: Foundations, control, algorithms, and experiments. J. Logic Prog. 41, 2&3, 231--277.
• 31: Jim des Rivières , Brian Cantwell Smith, The implementation of procedurally reflective languages, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.331-347, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802050]
• 32: Pascal Fradet , Daniel Le Métayer, Shape types, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.27-39, January 15-17, 1997, Paris, France [doi>10.1145/263699.263706]
• 33: Daniel P. Friedman , Mitchell Wand, Reification: Reflection without metaphysics, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.348-355, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802051]
• 34: Yoshihiko Futamura, Partial Evaluation of Computation Process—AnApproach to a Compiler-Compiler, Higher-Order and Symbolic Computation, v.12 n.4, p.381-391, December 1999 [doi>10.1023/A:1010095604496]
• 35: Yoshihiko Futamura, Partial Evaluation of Computation Process, Revisited, Higher-Order and Symbolic Computation, v.12 n.4, p.377-380, December 1999 [doi>10.1023/A:1010043619517]
• 36: 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.
• 37: J. P. Gallagher, Tutorial on specialisation of logic programs, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.88-98, June 14-16, 1993, Copenhagen, Denmark [doi>10.1145/154630.154640]
• 38: Steven E. Ganz , Amr Sabry , Walid Taha, Macros as multi-stage computations: type-safe, generative, binding macros in MacroML, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
• 39: Rakesh Ghiya , Laurie J. Hendren, Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in C, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-15, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237724]
• 40: Jürgen Giesl, Termination Analysis for Functional Programs using Term Orderings, Proceedings of the Second International Symposium on Static Analysis, p.154-171, September 25-27, 1995
• 41: Arne J. Glenstrup , Henning Makholm , Jens P. Secher, C-MIX: Specialization of C Programs, Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, p.108-154, June 29-July 10, 1998
• 42: Glenstrup, A. J. 1999. Terminator II: Stopping partial evaluation of fully recursive programs. M.S. thesis, DIKU, University of Copenhagen, DK-2100 Copenhagen ø.
• 43: Arne J. Glenstrup , Neil D. Jones, BTA Algorithms to Ensure Termination of Off-Line Partial Evaluation, Proceedings of the Second International Andrei Ershov Memorial Conference on Perspectives of System Informatics, p.273-284, June 25-28, 1996
• 44: Glück, R., Nakashige, R., and Zöchling, R. 1995. Binding-time analysis applied to mathematical algorithms. In System Modelling and Optimization, J. Doležal and J. Fidler, Eds. Chapman & Hall, London, England, 137--146.
• 45: Robert Glück , Morten Heine Sørensen, A Roadmap to Metacomputation by Supercompilation, Selected Papers from the Internaltional Seminar on Partial Evaluation, p.137-160, February 12-16, 1996
• 46: Brian Grant , Markus Mock , Matthai Philipose , Craig Chambers , Susan J. Eggers, DyC: an expressive annotation-directed dynamic compiler for C, Theoretical Computer Science, v.248 n.1-2, p.147-199, October 2000 [doi>10.1016/S0304-3975(00)00051-7]
• 47: Grobauer, B. 2001. Topics in semantics-based program manipulation. Ph.D. thesis, BRICS, Department of Computer Science, University of Aarhus, Aarhus, Denmark. DS-01-6.
• 48: Hatcliff, J., Mogensen, T. Æ., 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.
• 49: Holst, C. K. 1988. Poor man's generalization. Tech. Rep., DIKU, University of Copenhagen.
• 50: Carsten Kehler Holst, Finiteness Analysis, Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture, p.473-495, August 26-30, 1991
• 51: 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.
• 52: Paul Hudak, Building domain-specific embedded languages, ACM Computing Surveys (CSUR), v.28 n.4es, Dec. 1996 [doi>10.1145/242224.242477]
• 53: John Hughes, Type Specialisation for the lambda-Calculus; or, A New Paradigm for Partial Evaluation Based on Type Inference, Selected Papers from the Internaltional Seminar on Partial Evaluation, p.183-215, February 12-16, 1996
• 54: John Hughes , Lars Pareto , Amr Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.410-423, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.240882]
• 55: Stanley Jefferson , Daniel P. Friedman, A simple reflective interpreter, Lisp and Symbolic Computation, v.9 n.2-3, p.181-202, May/June 1996 [doi>10.1007/BF01806112]
• 56: Neil D. Jones, What Not to Do When Writing an Interpreter for Specialisation, Selected Papers from the Internaltional Seminar on Partial Evaluation, p.216-237, February 12-16, 1996
• 57: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 58: Neil D. Jones , Flemming Nielson, Abstract interpretation: a semantics-based tool for program analysis, Handbook of logic in computer science (vol. 4): semantic modelling, Oxford University Press, Oxford, 1995
• 59: Richard B. Kieburtz , Laura McKinney , Jeffrey M. Bell , James Hook , Alex Kotov , Jeffrey Lewis , Dino P. Oliva , Tim Sheard , Ira Smith , Lisa Walton, A software engineering experiment in software component generation, Proceedings of the 18th international conference on Software engineering, p.542-552, March 25-29, 1996, Berlin, Germany
• 60: Launchbury, J. 1991. Projection Factorisations in Partial Evaluation. Distinguished Dissertations in Computer Science. Cambridge University Press, Cambridge.
• 61: Julia L. Lawall , Peter Thiemann, Sound Specialization in the Presence of Computational Effects, Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software, p.165-190, September 23-26, 1997
• 62: Chin Soon Lee, Finiteness Analysis in Polynomial Time, Proceedings of the 9th International Symposium on Static Analysis, p.493-508, September 17-20, 2002
• 63: Lee, C. S. 2002b. Program termination analysis and termination of offline partial evaluation. Ph.D. thesis, University of Western Australia. Aug.
• 64: Chin Soon Lee , Neil D. Jones , Amir M. Ben-Amram, The size-change principle for program termination, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-92, January 2001, London, United Kingdom
• 65: Michael Leuschel, On the Power of Homeomorphic Embedding for Online Termination, Proceedings of the 5th International Symposium on Static Analysis, p.230-245, September 14-16, 1998
• 66: Michael Leuschel , Maurice Bruynooghe, Logic program specialisation through partial deduction: Control issues, Theory and Practice of Logic Programming, v.2 n.4, p.461-515, July 2002
• 67: Lindenstrauss, N. and Sagiv, Y. 1997. Automatic termination analysis of logic programs (with detailed experimental results). Unpublished. (http://www.cs.huji.ac.il/~naomil/.)
• 68: Naomi Lindenstrauss , Yehoshua Sagiv , Alexander Serebrenik, TermiLog: A System for Checking Termination of Queries to Logic Programs, Proceedings of the 9th International Conference on Computer Aided Verification, p.444-447, June 22-25, 1997
• 69: Yanhong A. Liu, Efficiency by Incrementalization: An Introduction, Higher-Order and Symbolic Computation, v.13 n.4, p.289-313, Dec. 1, 2000 [doi>10.1023/A:1026547031739]
• 70: J. W. Lloyd , J. C. Shepherdson, Partial evaluation in logic programming, Journal of Logic Programming, v.11 n.3-4, p.217-242, Oct./Nov. 1991 [doi>10.1016/0743-1066(91)90027-M]
• 71: 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.
• 72: Dylan McNamee , Jonathan Walpole , Calton Pu , Crispin Cowan , Charles Krasic , Ashvin Goel , Perry Wagle , Charles Consel , Gilles Muller , Renauld Marlet, Specialization tools and techniques for systematic optimization of system software, ACM Transactions on Computer Systems (TOCS), v.19 n.2, p.217-251, May 2001 [doi>10.1145/377769.377778]
• 73: Mogensen, T. Æ. 1988. Partially static structures in a self-applicable partial evaluator. In Partial Evaluation and Mixed Computation, D. Bjørner, A. Ershov, and N. Jones, Eds. Elsevier Science Publishers, North-Holland, Amsterdam, The Netherlands. 325--347.
• 74: Torben æ. Mogensen (Ed.), Glossary for Partial Evaluation and Related Topics, Higher-Order and Symbolic Computation, v.13 n.4, p.355-368, Dec. 1, 2000 [doi>10.1023/A:1026551132647]
• 75: Eugenio Moggi , Walid Taha , Zine-El-Abidine Benaissa , Tim Sheard, An Idealized MetaML: Simpler, and More Expressive, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.193-207, March 22-28, 1999
• 76: Flemming Nielson , Hanne Riis Nielson, Operational semantics of termination types, Nordic Journal of Computing, v.3 n.2, p.144-187, Summer 1996
• 77: Pareto, L. 2000. Types for crash prevention. Ph.D. dissertation. Chalmers University of Technology and Göteborg University, Göteborg, Sweden.
• 78: Péter, R. 1951. Rekursive Funktionen. Académiai Kiadó, Budapest, Hungary. (Translated and Printed as Recursive Function, Academic Press, New York, 1976).
• 79: Massimiliano Poletto , Wilson C. Hsieh , Dawson R. Engler , M. Frans Kaashoek, C and tcc: a language and compiler for dynamic code generation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.2, p.324-369, March 1999 [doi>10.1145/316686.316697]
• 80: A. Prasad Sistla , M. Y. Vardi , P. Wolper, The complementation problem for Bu¨chi automata with applications to temporal logic, Theoretical Computer Science, v.49 n.2-3, p.217-237, January 1987 [doi>10.1016/0304-3975(87)90008-9]
• 81: Ramsey, F. P. 1930. On a problem of formal logic. In Proceedings of the London Mathematical Society. Vol. 30. Cambridge University Press, Cambridge, U.K. 264--285.
• 82: Konstantinos Sagonas , Terrance Swift , David S. Warren, XSB as an efficient deductive database engine, Proceedings of the 1994 ACM SIGMOD international conference on Management of data, p.442-453, May 24-27, 1994, Minneapolis, Minnesota, United States
• 83: Ulrik Pagh Schultz, Partial Evaluation for Class-Based Object-Oriented Languages, Proceedings of the Second Symposium on Programs as Data Objects, p.173-197, May 21-23, 2001
• 84: Sestoft, P. 2001. Bibliography on partial evaluation and mixed computation. Tech. Rep., DIKU, University of Copenhagen, Copenhagen, Denmark.
• 85: 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.
• 86: Litong Song , Yoshihiko Futamura, A New Termination Approach for Specialization, Proceedings of the International Workshop on Semantics, Applications, and Implementation of Program Generation, p.72-91, September 20, 2000
• 87: Sørensen, M. H. and Glück, 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.
• 88: Chris Speirs , Zoltan Somogyi , Harald Søndergaard, Termination Analysis for Mercury, Proceedings of the 4th International Symposium on Static Analysis, p.160-171, September 08-10, 1997
• 89: Michael Sperber , Peter Thiemann, Generation of LR parsers by partial evaluation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.224-264, March 2000 [doi>10.1145/349214.349219]
• 90: Walid Mohamed Taha , Tim Sheard, Multistage programming: its theory and applications, 1999
• 91: Walid Taha, A sound reduction semantics for untyped CBN mutli-stage computation. Or, the theory of MetaML is non-trival (extended abstract), ACM SIGPLAN Notices, v.34 n.11, p.34-43, Nov. 1999
• 92: 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.
• 93: Walid Taha , Henning Makholm , John Hughes, Tag Elimination and Jones-Optimality, Proceedings of the Second Symposium on Programs as Data Objects, p.257-275, May 21-23, 2001
• 94: Walid Taha , Tim Sheard, MetaML and multi-stage programming with explicit annotations, Theoretical Computer Science, v.248 n.1-2, p.211-242, October 2000 [doi>10.1016/S0304-3975(00)00053-0]
• 95: Peter Thiemann, A Unified Framework for Binding-Time Analysis, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.742-756, April 14-18, 1997
• 96: Peter Thiemann, Aspects of the PGG System: Specialization for Standard Scheme, Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, p.412-432, June 29-July 10, 1998
• 97: V. F. Turchin, A supercompiler system based on the language REFAL, ACM SIGPLAN Notices, v.14 n.2, p.46-54, February 1979 [doi>10.1145/954063.954069]
• 98: Philip Wadler, Deforestation: Transforming Programs to Eliminate Trees, Proceedings of the 2nd European Symposium on Programming, p.344-358, March 21-24, 1988
• 99: Mitchell Wand , Daniel P. Friedman, The mystery of the tower revealed: a non-reflective description of the reflective tower, Proceedings of the 1986 ACM conference on LISP and functional programming, p.298-307, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319871]
• 100: Hongwei Xi, Dependent Types for Program Termination Verification, Higher-Order and Symbolic Computation, v.15 n.1, p.91-131, March 2002 [doi>10.1023/A:1019916231463]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.2 Automatic Programming

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Recursion
      D.3.4 Processors
          Subjects: Compilers; Interpreters; Optimization

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis; Partial evaluation
      F.3.3 Studies of Program Constructs
          Subjects: Program and recursion schemes

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program transformation

Keywords:
Binding-time analysis, quasitermination, size-change graphs, termination