Skip to main content
SpringerLink
Log in

Proving Properties about Functions on Lists Involving Element Tests

  • Conference paper
Recent Trends in Algebraic Development Techniques (WADT 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7137))

Included in the following conference series:

  • 361 Accesses

Abstract

Bundy and Richardson [4] 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. [7] 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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abbott, M., Altenkirch, T., Ghani, N.: Categories of Containers. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 23–38. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  2. Abbott, M., Altenkirch, T., Ghani, N.: Containers: Constructing strictly positive types. Theoretical Computer Science 342(1), 3–27 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  3. Bernardy, J.-P., Jansson, P., Claessen, K.: Testing Polymorphic Properties. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 125–144. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  4. Bundy, A., Richardson, J.: Proofs about Lists Using Ellipsis. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol. 1705, pp. 1–12. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  5. Jay, C.B.: A semantics for shape. Science of Computer Programming 25(2-3), 251–283 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  6. Peyton Jones, S.L. (ed.): Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press (2003)

    Google Scholar 

  7. Prince, R., Ghani, N., McBride, C.: Proving Properties about Lists Using Containers. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 97–112. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  8. Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Proc. of Information Processing, pp. 513–523. Elsevier (1983)

    Google Scholar 

  9. Wadler, P.: Theorems for free! In: Proc. of FPCA 1989, pp. 347–359. ACM (1989)

    Google Scholar 

  10. Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proc. of POPL 1989, pp. 60–76. ACM (1989)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Rheinische Friedrich-Wilhelms, Universität Bonn Institut für Informatik, Römerstraße 164, 53117, Bonn, Germany

    Daniel Seidel & Janis Voigtländer

Authors
  1. Daniel Seidel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Janis Voigtländer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DFKI, Cyber-Physical Systems, Deutsches Forschungszentrum für künstliche Intelligenz, 28359, Bremen, Germany

    Till Mossakowski

  2. Mathematik und Informatik, Universität Bremen, 28359, Bremen, Germany

    Hans-Jörg Kreowski

Rights and permissions

Reprints and permissions

Copyright information

© 2012 IFIP International Federation for Information Processing

About this paper

Cite this paper

Seidel, D., Voigtländer, J. (2012). Proving Properties about Functions on Lists Involving Element Tests. In: Mossakowski, T., Kreowski, HJ. (eds) Recent Trends in Algebraic Development Techniques. WADT 2010. Lecture Notes in Computer Science, vol 7137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28412-0_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-28412-0_17

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-28411-3

  • Online ISBN: 978-3-642-28412-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation