Lab 0: binary search trees

In this lab assignment, you will implement and prove the correctness of binary search trees. To do this assignment, download the source code and do all of the exercises, denoted by EXERCISE in that file.

If you are done with lab0 before the deadline (e.g., because you skipped the SF homeworks), then try the challenge.

To submit the lab assignment, create a .tar.gz file with your solution .v file(s), depending on whether you did the binary search tree assignment and/or the regex assignment:

% tar -zcf lab0-handin.tar.gz lab0btree.v lab0regex.v

and upload it to the submission web site (see link at the top of the page).

Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at

Creative Commons License