Title: Verifying the unification algorithm in LCF
First published: 1984