@inproceedings{Nipkow-ITP16,author={Tobias Nipkow},
title={Automatic Functional Correctness Proofs for Functional Search Trees},
booktitle={Interactive Theorem Proving (ITP 2016)},
editor={J. Blanchette and S. Merz},
publisher={Springer},series={LNCS},volume={9807},pages={307-322},year=2016}

@book{Okasaki,author="Chris Okasaki",title="Purely Functional Data Structures",
publisher="Cambridge University Press",year=1998}

@article{SleatorT-JACM85,author={Daniel D. Sleator and Robert E. Tarjan},
title={Self-adjusting Binary Search Trees},journal={J. ACM},
volume=32,number=3,pages={652-686},year=1985}
