Skip to content

bergwerf/skip_list

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

11 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

A functional skip list in ML

This is an implementation of a skip list key/value store in OCaml. The program is defined in a functional way to prepare it for verification using the Iris separation logic framework.

Skip lists resemble binary trees except that they do not require global rebalancing. Instead they rely on probabilistic heuristics to keep the time complexity logarithmic while only applying local modifications to the datastructure. This enables concurrent usage. Skip lists can be used to implement sets, key/value mappings, and indexed arrays.

About

A skip list in ML

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages