@inproceedings(AMARG2010,
 author       = "A. B. Avelar and F.L.C. de Moura and A. L. Galdino and M. Ayala-Rinc{\'o}n",
 year         = "2010",
 title        = "{Verification of the Completeness of Unification Algorithms {\`a} la Robinson}",
 booktitle    = "Proc. 17th Int. Workshop on Logic, Language, Information and Computation (WoLLIC)",
 series       = "LNCS",
 volume       = "6188",
 publisher    = "Springer",
 pages        = "110--124",
 doi          = "10.1007/978-3-642-13824-9\_10",
)
@book(BaNi98,
 author       = "F. Baader and T. Nipkow",
 year         = "1998",
 title        = "{Term Rewriting and {\em All That}}",
 publisher    = "Cambridge University Press",
)
@book(Te2003,
 editor       = "M. Bezem and J.W. Klop and R. de Vrijer",
 year         = "2003",
 title        = "{Term Rewriting Systems by TeReSe}",
 series       = "Cambridge Tracts in Theoretical Computer Science",
 volume       = "55",
 publisher    = "Cambridge University Press",
)
@unpublished(BlKo2011,
 author       = "F. Blanqui and A. Koprowski",
 year         = "2011",
 title        = "CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates",
 note         = "Available at {\tt http://color.inria.fr}",
)
@phdthesis(Bove1999,
 author       = "A. Bove",
 year         = "1999",
 title        = "Martin-L\"of Type Theory: Unification - A non-trivial Example",
 school       = "Chalmers University of Technology",
 note         = "Licentiate thesis",
)
@book(Bu98,
 author       = "S. N. Burris",
 year         = "1998",
 title        = "{Logic for Mathematics and Computer Science}",
 publisher    = "Prentice Hall",
)
@article(Constable09,
 author       = "R. Constable and W. Moczydlowski",
 year         = "2009",
 title        = "Extracting the resolution algorithm from a completeness proof for the propositional calculus",
 journal      = "Ann. of Pure and Appl. Logic",
 volume       = "161",
 number       = "3",
 pages        = "337--348",
 doi          = "10.1007/978-3-540-72734-7\_11",
)
@inproceedings(CoBi83,
 author       = "J. Corbin and M. Bidoit",
 year         = "1983",
 title        = "{A Rehabilitation of Robinson's Unification Algorithm}",
 booktitle    = "IFIP Congress",
 pages        = "909--914",
)
@book(EbFlTh84,
 author       = "H. D. Ebbinghaus and J. Flum and W. Thomas",
 year         = "1984",
 title        = "{Mathematical Logic}",
 publisher    = "Springer",
)
@article(GaAR2008c,
 author       = "A. L. Galdino and M. Ayala-Rinc{\'o}n",
 year         = "2008",
 title        = "{A Formalization of Newman's and Yokouchi Lemmas in a Higher-Order Language}",
 journal      = "Journal of Formalized Reasoning",
 volume       = "1",
 number       = "1",
 pages        = "39--50",
)
@inproceedings(GaAR2008b,
 author       = "A. L. Galdino and M. Ayala-Rinc{\'o}n",
 year         = "2009",
 title        = "{A PVS \emph {Theory} for Term Rewriting Systems}",
 booktitle    = "Proceedings of the Third Workshop on Logical and Semantic Frameworks, with Applications - LSFA 2008",
 series       = "Electronic Notes in Theoretical Computer Science",
 volume       = "247",
 pages        = "67--83",
 doi          = "10.1016/j.entcs.2009.07.049",
)
@article(GaAR2010,
 author       = "A. L. Galdino and M. Ayala-Rinc{\'o}n",
 year         = "2010",
 title        = "{A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem}",
 journal      = "J. Auto. Reas.",
 volume       = "45",
 number       = "3",
 pages        = "301--325",
 doi          = "10.1007/s10817-010-9165-2",
)
@article(Hi69,
 author       = "J.R. Hindley",
 year         = "1969",
 title        = "{The principal type-scheme of an object in combinatory logic}",
 journal      = "Trans. American Mathematical Society",
 volume       = "146",
 pages        = "29--60",
)
@book(Hi97,
 author       = "J.R. Hindley",
 year         = "1997",
 title        = "{Basic Simple Type Theory}",
 series       = "Cambridge Tracts in Theo. Computer Science",
 volume       = "42",
 publisher    = "CUP",
)
@inbook(KnBe70,
 author       = "D. E. Knuth and P. B. Bendix",
 year         = "1970",
 title        = "{Computational Problems in Abstract Algebra}",
 chapter      = "Simple Words Problems in Universal Algebras",
 pages        = "263--297",
 publisher    = "J. Leech, ed. Pergamon Press, Oxford, U. K.",
)
@inproceedings(KoCa2009,
 author       = "S. Kothari and J. Caldwell",
 year         = "2009",
 title        = "{A Machine Checked Model of MGU Axioms: Applications of Finite Maps and Functional Induction}",
 booktitle    = "23th Int. Workshop on Unification UNIF2009",
 pages        = "17--31",
)
@book(Llo87,
 author       = "J. W. Lloyd",
 year         = "1987",
 title        = "{Foundations of Logic Programming}",
 edition      = "second",
 series       = "Symbolic Computation -- Artificial Intelligence",
 publisher    = "Springer",
)
@article(Pa1985,
 author       = "Lawrence C. Paulson",
 year         = "1985",
 title        = "{Verifying the Unification Algorithm in LCF}",
 journal      = "Science of Computer Programming",
 volume       = "5",
 number       = "2",
 pages        = "143--169",
)
@article(Ro65,
 author       = "J. A. Robinson",
 year         = "1965",
 title        = "{A Machine-oriented Logic Based on the Resolution Principle}",
 journal      = "Journal of the ACM",
 volume       = "12",
 number       = "1",
 pages        = "23--41",
 doi          = "10.1145/321250.321253",
)
@techreport(Rou1992,
 author       = "J. Rouyer",
 year         = "1992",
 title        = "D\'eveloppement de l'Algorithme d'Unification dans le Calcul des Constructions",
 type         = "Technical Report",
 number       = "1795",
 institution  = "INRIA",
)
@article(RRMMAH2006,
 author       = "J.-L. Ruiz-Reina and F.-J. Mart\'{\i }n-Mateos J.-A. Alonso and M.-J. Hidalgo",
 year         = "2006",
 title        = "{Formal Correctness of a Quadratic Unification Algorithm}",
 journal      = "J. of Auto. Reas.",
 volume       = "37",
 number       = "1-2",
 pages        = "67--92",
 doi          = "10.1007/s10817-006-9030-5",
)