@MASTERSTHESIS\{IMM2017-07094,
    author       = "K. Hvidtfeldt",
    title        = "Formalized Unification Algorithms",
    year         = "2017",
    school       = "Technical University of Denmark, Department of Applied Mathematics and Computer Science",
    address      = "Richard Petersens Plads, Building 324, {DK-}2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk",
    type         = "",
    note         = "{DTU} supervisor: J{\o}rgen Villadsen, jovi@dtu.dk",
    url          = "http://www.compute.dtu.dk/English.aspx",
    abstract     = "The goal of the thesis is to implement a unification algorithm from the book {''}Term rewriting and all that{''} in the theorem prover Isabelle/{HOL,} so that proofs of termination and correctness can be formalized. In doing so the unification algorithm will be analyzed and compared to more traditional algorithms.

It will also give an opportunity to look at the challenges which arises when implementing, proving and the formalizations of algorithms in Isabelle/HOL."
}