2014/01/30 by Guyslain Naves, Naves, Guyslain, Arnaud Spiwack +1
Computer Science · #Data Structures and Algorithms (cs.DS) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.DS #cs.LO
paper · pdf · doi:10.48550/arxiv.1401.7886
To appear in proceedings of Interactive Theorem Proving (2014)
arxiv created 2014/06/13 · arxiv updated 2014/06/16
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.