Verified Memoization and Dynamic Programming

Simon Wimmer, Huwei Shu, Tobias Nipkow

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={?},pages={?-?},year=2018}