@article(amato:05,
 author       = {G. Amato and F. Scozzari},
 year         = {2009},
 title        = {Optimality in goal-dependent analysis of sharing},
 journal      = {Theory and Practice of Logic Programming},
 volume       = {9},
 number       = {5},
 pages        = {617--689},
 doi          = {10.1017/S1471068409990111},
)
@book(apt:book,
 author       = {K. R. Apt},
 year         = {1997},
 title        = {From logic programming to Prolog},
 publisher    = {Prentice Hall},
)
@article(apt:vanemden:82,
 author       = {K. R. Apt and M. H. van Emden},
 year         = {1982},
 title        = {Contributions to the theory of logic programming},
 journal      = {J.~of ACM},
 volume       = {29},
 number       = {3},
 pages        = {841--862},
 doi          = {10.1145/322326.322339},
)
@article(bol:92,
 author       = {R. N. Bol},
 year         = {1992},
 title        = {Generalizing completeness results for loop checks in logic programming},
 journal      = {Theor. Comp. Sci.},
 volume       = {104},
 number       = {1},
 pages        = {3--28},
 doi          = {10.1016/0304-3975(92)90164-B},
)
@article(doets:93,
 author       = {K. Doets},
 year         = {1993},
 title        = {{Levationis laus}},
 journal      = {J. Logic and Computation},
 volume       = {3},
 number       = {5},
 pages        = {487--516},
 doi          = {10.1093/logcom/3.5.487},
)
@article(eder:85,
 author       = {E. Eder},
 year         = {1985},
 title        = {Properties of substitutions and unifications},
 journal      = {J. Symbolic Computation},
 volume       = {1},
 number       = {1},
 pages        = {31--46},
 doi          = {10.1016/S0747-7171(85)80027-4},
)
@book(gallier,
 author       = {J. Gallier},
 year         = {2015},
 title        = {Logic for computer science: {F}oundations of automatic theorem proving},
 edition      = {2.},
 publisher    = {Dover},
)
@article(jacobs:langen:1992,
 author       = {D. Jacobs and A. Langen},
 year         = {1992},
 title        = {Static analysis of logic programs for independent {AND} parallelism},
 journal      = {J.~of Logic Programming},
 volume       = {13},
 number       = {2-3},
 pages        = {291 -- 314},
 doi          = {10.1016/0743-1066(92)90034-Z},
)
@inproceedings(KulasM:towcb,
 author       = {Kula\v{s}, M.},
 year         = {2005},
 title        = {Toward the concept of backtracking computation},
 editor       = {L. Aceto and W. J. Fokkink and I. Ulidowski},
 booktitle    = {Proc. of the Workshop on Structural Operational Semantics (SOS'04), London},
 series       = {ENTCS},
 volume       = {128},
 publisher    = {Elsevier},
 pages        = {39--59},
 doi          = {10.1016/j.entcs.2004.10.026},
)
@incollection(maher,
 author       = {J. L. Lassez and M. J. Maher and K. Marriott},
 year         = {1988},
 title        = {Unification revisited},
 editor       = {M. Boscarol and Carlucci Aiello, L. and G. Levi},
 booktitle    = {Foundations of Logic and Functional Programming},
 series       = {LNCS},
 volume       = {306},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {67--113},
 doi          = {10.1007/3-540-19129-1\_4},
)
@book(lloyd,
 author       = {J. W. Lloyd},
 year         = {1987},
 title        = {Foundations of logic programming},
 edition      = {2.},
 publisher    = {Springer-Verlag},
 doi          = {10.1007/978-3-642-83189-8},
)
@article(lloyd:shepherdson:91,
 author       = {J. W. Lloyd and J. C. Shepherdson},
 year         = {1991},
 title        = {Partial evaluation in logic programming},
 journal      = {J.~of Logic Programming},
 volume       = {11},
 number       = {3-4},
 pages        = {217--242},
 doi          = {10.1016/0743-1066(91)90027-M},
)
@inproceedings(catuscia:90,
 author       = {C. Palamidessi},
 year         = {1990},
 title        = {Algebraic properties of idempotent substitutions},
 booktitle    = {Proc. 17th ICALP},
 series       = {LNCS},
 volume       = {443},
 publisher    = {Springer-Verlag},
 pages        = {386--399},
 doi          = {10.1007/BFb0032046},
)
@phdthesis(plotkin:phd,
 author       = {G. D. Plotkin},
 year         = {1971},
 title        = {Automatic methods of inductive inference},
 school       = {U. of Edinburgh},
 url          = {http://homepages.inf.ed.ac.uk/gdp},
)
@inproceedings(pusch-wam,
 author       = {C. Pusch},
 year         = {1996},
 title        = {Verification of compiler correctness for the {WAM}},
 booktitle    = {Proc. {TPHOL}s},
 series       = {LNCS},
 volume       = {1125},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {347--361},
 doi          = {10.1007/BFb0105415},
)
@article(shep:94,
 author       = {J. C. Shepherdson},
 year         = {1994},
 title        = {The role of standardising apart in logic programming},
 journal      = {Theor. Comp. Sci.},
 volume       = {129},
 number       = {1},
 pages        = {143--166},
 doi          = {10.1016/0304-3975(94)90084-1},
)
@article(urban-unif,
 author       = {C. Urban and A. Pitts and M. Gabbay},
 year         = {2004},
 title        = {Nominal unification},
 journal      = {Theoretical Computer Science},
 volume       = {323},
 number       = {1-3},
 pages        = {473--497},
 doi          = {10.1016/j.tcs.2004.06.016},
 note         = {Proof on \url{http://www.inf.kcl.ac.uk/staff/urbanc/Unification/}.},
)