Interesting paper by Danvy on using fold-unfold lemmas in Coq, primarily based on his experience teaching functional programming + proofs. Would have been nicer with the Alectryon-hydras toolchain though, no source...
Last updated: Mar 28 2024 at 13:01 UTC