zbMATH — the first resource for mathematics

Verified memoization and dynamic programming. (English) Zbl 06947003
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].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI