==========
Coq is an interactive theorem prover.
These files are assignments and their solutions (my interpretation) for the course by Kevin Hamlin in UTD F13.
Use either coqide or coq proof assistant to load these. Alternatively if you are using linux use a compatible editor (emacs) with proper plugins to make it work.
The AVL Tree proof is the final project for the course. The proof is not efficient (as discussed with Dr. Hamlen) but atleast we managed to prove the tree.