+++
title = "Weakly embedded memoization"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3c1"]
forwardlinks = ["3c3c3"]
zettelid = "3c3c2"
+++

Memoization can also be weakly embedded in Coq by using co-inductive
datatypes. This works extremely well for functions that take Peano
numbers as input, as a lazy data structure can be defined using
co-inductive types, which represents unevaluated thunks. Once these are
evaluated, they can just be read back normally.