Proving Properties About Functions on Lists Involving Element Tests

Authors: D. Seidel and J. Voigtländer
Published: In 20th International Workshop on Algebraic Development Techniques (WADT'10), Schloss Etelsen, Germany, Revised Selected Papers (acceptance rate 15/32), volume 7137 of LNCS, pages 270-286, Springer, February 2012.
DOI: 10.1007/978-3-642-28412-0_17
BibTeX: SV12.bib
Abstract: Bundy and Richardson (LPAR'99) developed a method for reasoning about functions manipulating lists which is based on separating shape from content, and then exploiting a mathematically convenient representation for expressing shape-only manipulations. Later, Prince et al. (FLOPS'08) extended the technique to other data structures, and gave it a more formal basis via the theory of containers. All these results are restricted to fully polymorphic functions. For example, functions using equality tests on list elements are out of reach. We remedy this situation by developing new abstractions and representations for less polymorphic functions. In Haskell speak, we extend the earlier approach to be applicable in the presence of (certain) type class constraints.
Download: ProvingPropertiesAboutFunctionsOnListsInvolvingElementTests.pdf
Rights: Copyright held by Springer.