Traditional tree data structures provide logarithmic run-time access and manipulation to elements using a key. Here, we demonstrate how to adapt trees to operate on indices rather than keys. The resulting data structure provides a vector-like interface that achieves logarithmic lookup, insert, and deletion – as compared to the linear insertion and deletion run-time for vectors. Furthermore, we demonstrate how the data structure can be further modified to implement efficient manipulation of large text buffers.

Type systems have been successfully used to statically catch errors, like dividing an integer with a boolean. Still, well typed programs can go wrong, for example, with a division by zero resulting in a run-time exception!

Liquid Types enrich existing type systems with logical predicates and let you specify and automatically verify semantic properties of your code.