Verified Memoization and Dynamic Programming
We present a lightweight framework in Isabelle/HOL for the automatic verified (functional or imperative) memoization of recursive functions. Our tool constructs a memoized version of the recursive function and proves a correspondence theorem between the two functions. 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 classic dynamic programming problems.
pdf
BibTeX:
@inproceedings{WimmerHN-ITP18,
author={Simon Wimmer and Shuwei Hu and Tobias Nipkow},
title={Verified Memoization and Dynamic Programming},
booktitle={Interactive Theorem Proving (ITP 2018)},
editor={J. Avigad and A. Mahboubi},
publisher=Springer,series=LNCS,volume={10895},pages={579--596},year=2018}