This repository is a project that I and Oscar Toro did for the Programming Languages Seminar course at ITU.
It is an implementation and verification of the Finger Tree data-structure, first popularized by Hinze and Paterson. There is a report in this repo with references and explanation.
The verification was actually quite challenging due to polymorphic recursion! But also a very fun learning experience.