Verifying the Unification Algorithm in LCF
<|reference_start|>Verifying the Unification Algorithm in LCF: 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.<|reference_end|>
@article{paulson2000verifying,
    title={Verifying the Unification Algorithm in LCF},
    author={Lawrence C. Paulson},
    journal={Science of Computer Programming 5 (1985), 143-170},
    year={2000},
    archivePrefix={arXiv},
    eprint={cs/9301101},
    primaryClass={cs.LO}
}