Balancing lists: a proof pearl
Se ha publicado un artículo de razonamiento formalizado en Coq sobre algorítmica titulado Balancing lists: a proof pearl.
Sus autores son Guyslain Naves (de la Aix-Marseille University) y Arnaud Spiwack (de Inria Paris-Rocquencourt).
Su resumen es
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.
El código de las correspondientes teorías en Coq se encuentra aquí.