Paulson, Lawrence "Verifying the unification algorithm in LCF" Technical Report UCAM-CL-TR-50 March 1984
(1984)
Languages mentioned
Cambridge LCF
{1982}
LCF
{1972} Logic for Computable Functions