Skip to Main content Skip to Navigation
New interface
Conference papers

Balancing Lists: A Proof Pearl

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.
Complete list of metadata

Cited literature [4 references]  Display  Hide  Download

https://hal.inria.fr/hal-01097937
Contributor : Arnaud Spiwack Connect in order to contact the contributor
Submitted on : Monday, December 22, 2014 - 2:39:12 PM
Last modification on : Thursday, March 17, 2022 - 10:08:44 AM
Long-term archiving on: : Monday, March 23, 2015 - 7:30:33 PM

File

Balancing%20lists.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Collections

Citation

Guyslain Naves, Arnaud Spiwack. Balancing Lists: A Proof Pearl. 5th International Conference, ITP 2014, Jul 2014, Vienna, Austria. pp.437 - 449, ⟨10.1007/978-3-319-08970-6_28⟩. ⟨hal-01097937⟩

Share

Metrics

Record views

190

Files downloads

84