| 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. |