Agerholm, S. (1994). A HOL Basis for Reasoning about Functional Programs. BRICS Report Series, 1(44). https://doi.org/10.7146/brics.v1i44.21598