Balancing lists: a proof pearl
Data Structures and Algorithms
2014-06-16 v2 Logic in Computer Science
Abstract
Starting with an algorithm to turn lists into full trees which uses non-obvious invariants and partial functions, we progressively encode the invariants in the types of the data, removing most of the burden of a correctness proof. The invariants are encoded using non-uniform inductive types which parallel numerical representations in a style advertised by Okasaki, and a small amount of dependent types.
Cite
@article{arxiv.1401.7886,
title = {Balancing lists: a proof pearl},
author = {Guyslain Naves and Arnaud Spiwack},
journal= {arXiv preprint arXiv:1401.7886},
year = {2014}
}
Comments
To appear in proceedings of Interactive Theorem Proving (2014)