Skip to content

Left-leaning red-black trees in Agda (insertion and deletion) with static ordering and balancing invariants

Notifications You must be signed in to change notification settings

andreasabel/red-black-tree-left-leaning

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Left-leaning red-black trees in Agda

This is an implementation of red-black trees (aka 2-3-4 trees) in Agda with static balancing and ordering invariants. Insertion and deletion are implemented, the latter just for left-leaning red-black trees (aka 2-3 trees).

The development was mostly carried out by Julien Oster as a student research project at LMU Munich in 2009/2010.

The main development resides in LLRBTree.agda.

The implementation of the ordering invariant predates the seminal paper by Conor McBride, Keeping your neighbours in order (ICFP 2010). The techniques of McBride would considerably simplify the development.

About

Left-leaning red-black trees in Agda (insertion and deletion) with static ordering and balancing invariants

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published