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 in 0 Serials

Citations by Year