On 2 August 2009, Sunil Kothari, a Ph.D. candidate in the Computer Science Department, presented a paper co-authored with Professor Caldwell at the UNIF09 meeting in Montreal Canada. The paper was titled "A Machine Checked Model of MGU Axioms: Applications of Finite Maps and Functional Induction". In the paper Kothari and Caldwell describe a formal proof/verification in the Coq theorm prover of a model of the axioms for most general unifiers. This is part of a larger effort to formally verify the correctness of Type Inference algorithms of the kind used in advanced functional programming languages like Haskell and Ocaml. This work reported on in the paper is part of Mr. Kothari's Ph.D. research. Mr. Kothari's work was partially supported by an NSF Science of Design grant (NSF 0613919) which explores the idea that comprehensibility of a software design can be used as a criteria of goodness. Comprehensibility is characterized by the ease with which formal logic based tools can be used to verify and transform software artifacts.