1. E. Albert, J. Gallagher, M. Gomes-Zamalla & G. Puebla (2009): Type-based Homeomorphic Embedding for Online Termination. Journal of Information Processing Letters 109(15), pp. 879–886, doi:10.1016/j.ipl.2009.04.016.
  2. D. Caucal (1992): On the regular structure of prefix rewriting. Theoretical Computer Science 106, pp. 61–86, doi:10.1016/0304-3975(92)90278-N.
  3. S. Greibach (1965): A New Normal-Form Theorem for Context-Free Phrase Structure Grammars. Journal of the ACM 12(1), doi:10.1145/321250.321254.
  4. G. W. Hamilton & N. D. Jones (2012): Distillation with labelled transition systems, pp. 15–24. IEEE Computer Society Press, doi:10.1145/2103746.2103753.
  5. J. E. Hopcroft & J. D. Ullman (1979): Introduction to Automata Theory, Languages, and Computation. Addison-Wesley.
  6. A.K. Joshi, K.V. Shanker & D. Weir (1990): The Convergence of Mildly Context-Sensitive Grammar Formalisms. Technical Report No. MS-CIS-90-01, University of Pennsylvania. Available at
  7. I. Klyuchnikov (2010): Inferring and Proving Properties of Functional Programs by Means of Supercompilation. Ph. D. Thesis (in Russian), Keldysh Institute of Applied Mathematics of RAS, Moscow. Available at
  8. J.B. Kruskal (1960): Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture. Transactions of the American Mathematical Society 95, pp. 210–225, doi:10.2307/1993287.
  9. M. Leuschel (2002): Homeomorphic Embedding for Online Termination of Symbolic Methods, pp. 379–403, Lecture Notes in Computer Science 2566. IEEE Computer Society Press, doi:10.1007/3-540-36377-7_17.
  10. C. St. J. A. Nash-Williams (1965): On Well-quasi-ordering Infinite Trees. Proceedings of Cambridge Philosophical Society 61, pp. 697–720, doi:10.1017/s0305004100039062.
  11. A. P. Nemytykh (2007): The Supercompiler Scp4: General Structure. URSS, Moscow. (In Russian).
  12. A. Nepeivoda (2014): Turchin's Relation and Subsequence Relation in Loop Approximation. In: PSI 2014. Ershov Informatics Conference. Poster Session 23. EPiC Series, EasyChair, pp. 30–42. Available at
  13. L. Puel (1989): Using Unavoidable Set of Trees to Generalize Kruskal's Theorem. Journal of Symbolic Computation 8, pp. 335–382, doi:10.1016/s0747-7171(89)80035-5.
  14. Y. Saouter (1995): Halting Problem for One-State Turing Machines. Research Report RR-2577, INRIA. Available at
  15. M. H. Sørensen & R. Glück (1995): An Algorithm of Generalization in Positive Supercompilation. In: Proceedings of ILPS'95, the International Logic Programming Symposium. MIT Press, pp. 465–479. Available at
  16. M.H. Sørensen (1994): Turchin's Supercompiler Revisited. Ms.Thesis, Department of Computer Science, University of Copenhagen. Available at
  17. M.H. Sørensen, R. Glück & N. D. Jones (1996): A Positive Supercompiler. Journal of Functional Programming 6, pp. 811–838, doi:10.1017/s0956796800002008.
  18. V. F. Turchin (1986): The Concept of a Supercompiler. ACM Transactions on Programming Languages and Systems 8(3), pp. 292–325, doi:10.1145/5956.5957.
  19. V. F. Turchin (1989): Refal-5, Programming Guide and Reference Manual. New England Publishing Co., Holyoke, Massachusetts. Electronic version:
  20. V.F. Turchin (1988): The algorithm of generalization in the supercompiler. Partial Evaluation and Mixed Computation, pp. 341–353.

Comments and questions to:
For website issues: