Source code repo for the master thesis "Verification and Theorem proving in F*" (Sebastian Sturm)

• RBTree: A verified implementation of insertion and deletion into and from red-black trees following C. Okasaki. Red-black trees in a functional setting. Journal of Functional Programming, 1, Jan. 1993.
• PoplmarkReloaded: A (incomplete) solution to B. Pientka. Poplmark reloaded: Mechanizing logical relations proofs (invited talk). In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pages 1–1, New York, NY, USA, 2018. ACM. ISBN 978-1-4503-5586-5. doi: 10.1145/ 3167102. URL http://doi.acm.org/10.1145/3167102.