[isabelle] New in the AFP: Monadification, Memoization and Dynamic Programming

This new entry by Simon Wimmer, Shuwei Hu and Tobias Nipkow is now online at


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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.