Verifying weight biased leftist heaps using dependent types
Tutorial paper "Verifying weight biased leftist heaps using dependent types" + companion code. This paper has not been published in any peer-reviewed journal.
Code is located in
src/ directory containing three subdirectories:
Basics- modules defining
Order, basic functions for equational reasoning and proofs of elementary properties (like associativity and commutatibity of addition).
TwoPassMerge- implementation of weight biased leftist heaps based on a two-pass merging algorithm. Merging uses helper function
SinglePassMerge- implementation based on a single-pass merging obtained by inlining all calls to
Latest version of the source code is available on BitBucket.
See LICENSE file for code license.