Agerholm, S. A HOL Basis for Reasoning about Functional Programs. BRICS 1994, 1.