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 .
- Wimmer, S., Hu, S., & Nipkow, T. (2018). Verified Memoization and Dynamic Programming. Lecture Notes in Computer Science, 579–596. https://doi.org/10.1007/978-3-319-94821-8_34