### Abstract

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].

### License

BSD License

### Topics

- Computer science/Algorithms
- Computer science/Functional programming

### Related publications

- Wimmer, S., Hu, S., & Nipkow, T. (2018). Verified Memoization and Dynamic Programming. Lecture Notes in Computer Science, 579–596. https://doi.org/10.1007/978-3-319-94821-8_34

### Session Monad_Memo_DP

- State_Monad_Ext
- Pure_Monad
- DP_CRelVS
- State_Heap_Misc
- Heap_Monad_Ext
- State_Heap
- DP_CRelVH
- Memory
- Pair_Memory
- Indexing
- Memory_Heap
- Transform_Cmd
- Bottom_Up_Computation
- Bottom_Up_Computation_Heap
- Solve_Cong
- Heap_Main
- State_Main
- Example_Misc
- Tracing
- Ground_Function
- Bellman_Ford
- Heap_Default
- Knapsack
- Counting_Tiles
- CYK
- Min_Ed_Dist0
- OptBST
- Longest_Common_Subsequence
- All_Examples

### Depends on

- Haskell’s Show Class in Isabelle/HOL

### Used by

- Optimal Binary Search Trees
- Hidden Markov Models

### Auto-related entries

- Simple Firewall
- Verification of the UpDown Scheme
- Information Flow Noninterference via Slicing
- Inter-Procedural Information Flow Noninterference via Slicing

## Cite

×

Monad_Memo_DP-AFP

    @article{Monad_Memo_DP-AFP,
      author  = {Simon Wimmer and Shuwei Hu and Tobias Nipkow},
      title   = {Monadification, Memoization and Dynamic Programming},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Monad_Memo_DP.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Feb 13, 2022 : Isabelle2021-1
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- May 23, 2018 : Isabelle2017