Verified memoization and dynamic programming. (English) Zbl 1511.68094

Wimmer, Simon; Hu, Shuwei; Nipkow, Tobias

Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 579-596 (2018).

Summary: 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 representative dynamic programming problems.
For the entire collection see [Zbl 1391.68001].

MSC:

68N30	Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
90C39	Dynamic programming

Software:

VerifyThis; Memoization; Coq; Isabelle/HOL