Monadification, Memoization and Dynamic Programming

Simon Wimmer ๐ŸŒ, Shuwei Hu ๐Ÿ“ง and Tobias Nipkow ๐ŸŒ

May 22, 2018

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

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].

License

BSD License

Topics

Related publications

Session Monad_Memo_DP