@MASTERSTHESIS\{IMM2018-07091,
    author       = "K. F. Brandt",
    title        = "Formalization of a near-linear time algorithm for solving the unification problem",
    year         = "2018",
    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",
    abstract     = "This thesis deals with formal verification of an imperatively formulated algorithm for solving first-order syntactic unification based on sharing of terms by storing them in a {DAG}. A theory for working with the relevant data structures is developed and a part of the algorithm is shown equivalent with a functional formulation."
}