Monad as modality
method to extract a monad-based imperative functional program from a proof
scientific article; zbMATH DE number 1178779