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.
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.
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.
G. W. Hamilton & N. D. Jones (2012):
Distillation with labelled transition systems,
pp. 15–24.
IEEE Computer Society Press,
doi:10.1145/2103746.2103753.
J. E. Hopcroft & J. D. Ullman (1979):
Introduction to Automata Theory, Languages, and Computation.
Addison-Wesley.
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 http://repository.upenn.edu/cis_reports/539.
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 http://keldysh.ru/council/1/klyuchnikov-diss.pdf.
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.
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.
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.
A. P. Nemytykh (2007):
The Supercompiler Scp4: General Structure.
URSS, Moscow.
(In Russian).
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.
Y. Saouter (1995):
Halting Problem for One-State Turing Machines.
Research Report RR-2577, INRIA.
Available at https://hal.inria.fr/inria-00074105.
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 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.1869.
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.
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.
V. F. Turchin (1989):
Refal-5, Programming Guide and Reference Manual.
New England Publishing Co.,
Holyoke, Massachusetts.
Electronic version:http://www.botik.ru/pub/local/scp/refal5/.
V.F. Turchin (1988):
The algorithm of generalization in the supercompiler.
Partial Evaluation and Mixed Computation,
pp. 341–353.