Proof-producing translation of higher-order logic into pure and stateful ML
scientific article; zbMATH DE number 6330158