Comment by nanomonkey

I've been looking for the same for scheme and clojure. Here are a few I've found:

Functional Data Structures and Algorithms, A Proof Assistant Approach by Tobias Nipkow (Ed.) [https://fdsa-book.net/functional_data_structures_algorithms....]

Purely Functional Data Structures thesis by Chris Okasaki [https://www.cs.cmu.edu/~rwh/students/okasaki.pdf]

https://en.wikipedia.org/wiki/Purely_functional_data_structu...