Stream: Hydras & Co. universe

Topic: Fold-unfold Coq tutorial


view this post on Zulip Karl Palmskog (Oct 05 2022 at 20:01):

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