Binary Search Trees

Viktor Kuncak 🌐

April 5, 2004

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


The correctness is shown of binary search tree operations (lookup, insert and remove) implementing a set. Two versions are given, for both structured and linear (tactic-style) proofs. An implementation of integer-indexed maps is also verified.


BSD License


Session BinarySearchTree