Balancing Lists: A Proof Pearl

Guyslain Naves 1 Arnaud Spiwack 2
2 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt
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 metadatas

Cited literature [4 references]  Display  Hide  Download

https://hal.inria.fr/hal-01097937
Contributor : Arnaud Spiwack <>
Submitted on : Monday, December 22, 2014 - 2:39:12 PM
Last modification on : Monday, March 4, 2019 - 2:04:14 PM
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

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

404

Files downloads

124