@article(Albert,
 author       = {E. Albert and J. Gallagher and Gomes-Zamalla, M. and G. Puebla},
 year         = {2009},
 title        = {Type-based Homeomorphic Embedding for Online Termination},
 journal      = {Journal of Information Processing Letters},
 volume       = {109},
 number       = {15},
 pages        = {879--886},
 doi          = {10.1016/j.ipl.2009.04.016},
)
@article(Caucal,
 author       = {D. Caucal},
 year         = {1992},
 title        = {On the regular structure of prefix rewriting},
 journal      = {Theoretical Computer Science},
 volume       = {106},
 pages        = {61--86},
 doi          = {10.1016/0304-3975(92)90278-N},
)
@article(Greibach,
 author       = {S. Greibach},
 year         = {1965},
 title        = {A New Normal-Form Theorem for Context-Free Phrase Structure Grammars},
 journal      = {Journal of the ACM},
 volume       = {12},
 number       = {1},
 doi          = {10.1145/321250.321254},
)
@inbook(Hamilton,
 author       = {G. W. Hamilton and N. D. Jones},
 year         = {2012},
 title        = {Distillation with labelled transition systems},
 pages        = {15--24},
 publisher    = {IEEE Computer Society Press},
 doi          = {10.1145/2103746.2103753},
)
@book(HopcroftUlmanBook,
 author       = {J. E. Hopcroft and J. D. Ullman},
 year         = {1979},
 title        = {Introduction to Automata Theory, Languages, and Computation},
 publisher    = {Addison-Wesley},
)
@misc(Joshi,
 author       = {A.K. Joshi and K.V. Shanker and D. Weir},
 year         = {1990},
 title        = {The Convergence of Mildly Context-Sensitive Grammar Formalisms},
 howpublished = {Technical Report No. MS-CIS-90-01, University of Pennsylvania},
 url          = {http://repository.upenn.edu/cis_reports/539},
)
@misc(Kluch,
 author       = {I. Klyuchnikov},
 year         = {2010},
 title        = {Inferring and Proving Properties of Functional Programs by Means of Supercompilation},
 howpublished = {Ph. D. Thesis (in Russian), Keldysh Institute of Applied Mathematics of RAS, Moscow},
 url          = {http://keldysh.ru/council/1/klyuchnikov-diss.pdf},
)
@article(Kruskal,
 author       = {J.B. Kruskal},
 year         = {1960},
 title        = {Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture},
 journal      = {Transactions of the American Mathematical Society},
 volume       = {95},
 pages        = {210--225},
 doi          = {10.2307/1993287},
)
@inbook(Leuschel,
 author       = {M. Leuschel},
 year         = {2002},
 title        = {Homeomorphic Embedding for Online Termination of Symbolic Methods},
 pages        = {379--403},
 series       = {Lecture Notes in Computer Science},
 volume       = {2566},
 publisher    = {IEEE Computer Society Press},
 doi          = {10.1007/3-540-36377-7\_17},
)
@article(NW65,
 author       = {Nash-Williams, C. St. J. A.},
 year         = {1965},
 title        = {On Well-quasi-ordering Infinite Trees},
 journal      = {Proceedings of Cambridge Philosophical Society},
 volume       = {61},
 pages        = {697--720},
 doi          = {10.1017/s0305004100039062},
)
@book(NemytykhBook,
 author       = {A. P. Nemytykh},
 year         = {2007},
 title        = {The Supercompiler Scp4: General Structure},
 publisher    = {URSS, Moscow},
 note         = {(In Russian)},
)
@inproceedings(ANNTur,
 author       = {A. Nepeivoda},
 year         = {2014},
 title        = {Turchin's Relation and Subsequence Relation in Loop Approximation},
 booktitle    = {PSI 2014. Ershov Informatics Conference. Poster Session},
 volume       = {23},
 publisher    = {EPiC Series, EasyChair},
 pages        = {30--42},
 url          = {http://www.easychair.org/publications/download/Turchin_s_Relation_and_Subsequence_Relation_in_Loop_Approximation},
)
@article(Puel,
 author       = {L. Puel},
 year         = {1989},
 title        = {Using Unavoidable Set of Trees to Generalize Kruskal's Theorem},
 journal      = {Journal of Symbolic Computation},
 volume       = {8},
 pages        = {335--382},
 doi          = {10.1016/s0747-7171(89)80035-5},
)
@misc(OneStateTM,
 author       = {Y. Saouter},
 year         = {1995},
 title        = {Halting Problem for One-State Turing Machines},
 howpublished = {Research Report RR-2577, INRIA},
 url          = {https://hal.inria.fr/inria-00074105},
)
@inproceedings(Gluck95,
 author       = {S\o{}rensen, M. H. and R. Gl\"uck},
 year         = {1995},
 title        = {An Algorithm of Generalization in Positive Supercompilation},
 booktitle    = {Proceedings of ILPS'95, the International Logic Programming Symposium},
 publisher    = {MIT Press},
 pages        = {465--479},
 url          = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.1869},
)
@misc(SorensenMsTh,
 author       = {S\o{}rensen, M.H.},
 year         = {1994},
 title        = {Turchin's Supercompiler Revisited},
 howpublished = {Ms.Thesis, Department of Computer Science, University of Copenhagen},
 url          = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.50.8214&rep=rep1&type=pdf},
)
@article(Jones,
 author       = {S\o{}rensen, M.H. and R. Gl\"uck and N. D. Jones},
 year         = {1996},
 title        = {A Positive Supercompiler},
 journal      = {Journal of Functional Programming},
 volume       = {6},
 pages        = {811--838},
 doi          = {10.1017/s0956796800002008},
)
@article(Tur86,
 author       = {V. F. Turchin},
 year         = {1986},
 title        = {The Concept of a Supercompiler},
 journal      = {ACM Transactions on Programming Languages and Systems},
 volume       = {8},
 number       = {3},
 pages        = {292--325},
 doi          = {10.1145/5956.5957},
)
@book(TurRefal5,
 author       = {V. F. Turchin},
 year         = {1989},
 title        = {Refal-5, Programming Guide and Reference Manual},
 publisher    = {New England Publishing Co.},
 address      = {Holyoke, Massachusetts},
 note         = {Electronic version:\url{http://www.botik.ru/pub/local/scp/refal5/}},
)
@article(Turchin88,
 author       = {V.F. Turchin},
 year         = {1988},
 title        = {The algorithm of generalization in the supercompiler},
 journal      = {Partial Evaluation and Mixed Computation},
 pages        = {341--353},
)