Memoization swMATH ID: 28640 Software Authors: Simon Wimmer, Shuwei Hu,Tobias Nipkow Description: Monadification, Memoization and Dynamic Programming. We present a lightweight framework for the automatic verified (functional or imperative) memoization of recursive functions. Our tool can turn a pure Isabelle/HOL function definition into a monadified version in a state monad or the Imperative HOL heap monad, and prove a correspondence theorem. We provide a variety of memory implementations for the two types of monads. A number of simple techniques allow us to achieve bottom-up computation and space-efficient memoization. The framework’s utility is demonstrated on a number of representative dynamic programming problems. A detailed description of our work can be found in the accompanying paper [2]. Homepage: https://www.isa-afp.org/entries/Monad_Memo_DP.html Dependencies: Isabelle Related Software: VerifyThis; Isabelle/HOL; Coq Cited in: 1 Document Cited by 3 Authors 1 Hu, Shuwei 1 Nipkow, Tobias 1 Wimmer, Simon Cited in 0 Serials Cited in 2 Fields 1 Computer science (68-XX) 1 Operations research, mathematical programming (90-XX) Citations by Year