The semantics of PASCAL in LCF.