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.
Type de document :
Communication dans un congrès
5th International Conference, ITP 2014, Jul 2014, Vienna, Austria. 8558, pp.437 - 449, 2014, Interactive Theorem Proving. 〈10.1007/978-3-319-08970-6_28〉
Liste complète des métadonnées

Littérature citée [4 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01097937
Contributeur : Arnaud Spiwack <>
Soumis le : lundi 22 décembre 2014 - 14:39:12
Dernière modification le : vendredi 25 mai 2018 - 12:02:07
Document(s) archivé(s) le : lundi 23 mars 2015 - 19:30:33

Fichier

Balancing%20lists.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

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

Partager

Métriques

Consultations de la notice

349

Téléchargements de fichiers

56