Department of Computer Science and Technology

Technical reports

Verifying the unification algorithm in LCF

Lawrence Paulson

March 1984, 28 pages

DOI: 10.48456/tr-50


Manna and Waldinger’s theory of substitutions and unification has been verified using the Cambridge LCF theorem prover. A proof of the monotonicity of substitution is presented in detail, as an example of interaction with LCF. Translating the theory into LCF’s domain-theoretic logic is largely straightforward. Well-founded induction on a complex ordering is translated into nested structural inductions. Correctness of unification is expressed using predicates for such properties as idempotence and most-generality. The verification is presented as a series of lemmas. The LCF proofs are compared with the original ones, and with other approaches. It appears difficult to find a logic that is both simple and flexible, especially for proving termination.

Full text

PDF (0.2 MB)
DVI (0.0 MB)

BibTeX record

  author =	 {Paulson, Lawrence},
  title = 	 {{Verifying the unification algorithm in LCF}},
  year = 	 1984,
  month = 	 mar,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-50},
  number = 	 {UCAM-CL-TR-50}