Balancing Lists: A Proof Pearl

DOI10.1007/978-3-319-08970-6_28MaRDI QIDQ2879268zbMATH OpenOpenAlexFDO

Authors Guyslain Naves, Arnaud Spiwack

Publication date 8 September 2014

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1401.7886

Mathematics Subject Classification ID

Data structures (68P05)

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.

Recommendations

• Proof pearl: The KeY to correct and stable sorting
• scientific article; zbMATH DE number 1405440
• scientific article; zbMATH DE number 4045132
• Padded Lists Revisited
• scientific article; zbMATH DE number 524124
• Balcobalancing numbers and balcobalancers
• Almost balancing numbers
• On the theory of bags and lists
• scientific article; zbMATH DE number 6957541
• scientific article; zbMATH DE number 3865598

Cited in

(4)

• How to keep your neighbours in order
• Padded Lists Revisited
• scientific article; zbMATH DE number 1405440 (Why is no real title available?)
• On the Implementation of Construction Functions for Non-free Concrete Data Types

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Balancing Lists: A Proof Pearl

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2879268)