Example of programming with indexed types: binary search trees - a podcast by Aaron Stump

The example of binary search trees where we use indices to enforce the bst property statically

Further episodes of Iowa Type Theory Commute

Further podcasts by Aaron Stump

Website of Aaron Stump