Skip to main content
SpringerLink
Log in

Theorem Proving for Functional Programmers

Sparkle: A Functional Theorem Prover

  • Conference paper
  • First Online:
Implementation of Functional Languages (IFL 2001)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2312))

Included in the following conference series:

Abstract

Sparkle is a new theorem prover written in and specialized for the functional programming language Clean. It is mainly intended to be used by programmers for proving properties of parts of programs, combining programming and reasoning into one process. It can also be used by logicians interested in proving properties of larger programs.

Two features of Sparkle are in particular helpful for programmers. Firstly, Sparkle is integrated in Clean and has a semantics based on lazy graph-rewriting. This allows reasoning to take place on the program itself, rather than on a translation that uses di.erent concepts. Secondly, Sparkle supports automated reasoning. Trivial goals will automatically be discarded and suggestions will be given on more difficult goals.

This paper presents a small example proof built in Sparkle. It will be shown that building this proof is easy and requires little effort.

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. P. Achten and M. Wierich. A Tutorial to the CLEAN Object I/O Library (version 1.2), Nijmegen, February 2000. CSI Technical Report, CSI-R0003.

    Google Scholar 

  2. E. Barendsen and S. Smetsers. Strictness Typing, Nijmegen, 1998. In proceedings of the 10th International Workshop on Implementation of Functional Languages (IFL’98), London, 1998, pages 101–116.

    Google Scholar 

  3. R. Bird. Introduction to Functional Programming using Haskell, second edition, Prentice Hall Europe, 1998, ISBN 0-13-484346-0.

    Google Scholar 

  4. A. Butterfield and G. Strong. Proving Correctness of Programs with I/O-a paradigm comparison, Dublin, 2001. In proceedings of the 13th InternationalWorkshop on Implementation of Functional Languages (IFL’01), Stockholm, 2001, pages 319–334.

    Google Scholar 

  5. The Coq Development Team. The Coq Proof Assistant Reference Manual (version 7.0), Inria, 1998. http://pauillac.inria.fr/coq/doc/main.html

  6. M. van Eekelen and R. Plasmeijer. Concurrent Clean Language Report (version 1.3), Nijmegen, June 1998. CSI Technical Report, CSI-R9816. http://www.cs.kun.nl/~clean/Manuals/manuals.html

  7. T. Noll, L. Fredlund and D. Gurov. The EVT Erlang Verification Tool, Stockholm, 2001. In proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01), Lecture Notes in Computer Science, Vol. 2031, Springer, 2001, ISBN 3-540-41865-2, pages 582–585.

    Google Scholar 

  8. S. Mintchev. Mechanized reasoning about functional programs, Manchester, 1994. In K. Hammond, D.N. Turner and P. Sansom, editors, Functional Programming, Glasgow 1994, pages 151–167. Springer-Verlag.

    Google Scholar 

  9. M. de Mol and M. van Eekelen. A proof tool dedicated to Clean-the first prototype, 1999. In proceedings of Applications of Graph Transformations with Industrial Relevance 1999, Lecture Notes in Computer Science, Vol. 1779, Springer, 2000, ISBN 3-540-67658-9, pages 271–278.

    Google Scholar 

  10. S. Owre, N. Shankar, J.M. Rushby and D.W.J. Stringer-Calvert. PVS Language Reference (version 2.3), 1999. http://pvs.csl.sri.com/manuals.html

  11. L. C. Paulson. Logic and Computation, Cambridge University Press, 1987. ISBN 0-52-134632-0.

    Google Scholar 

  12. L. C. Paulson. The Isabelle Reference Manual, Cambridge, 2001. http://www.cl.cam.ac.uk/Research/HVG/Isabelle/docs.html

  13. S. Peyton Jones(editor), J. Hughes(editor) et al. Report on the programming language Haskell 98, Yale, 1999. http://www.haskell.org/definition/

  14. N. Winstanley. Era User Manual, version 2.0, Glasgow, 1998. http://www.dcs.gla.ac.uk/~nww/Era/Era.html

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Nijmegen, the Netherlands

    Maarten de Mol, Marko van Eekelen & Rinus Plasmeijer

Authors
  1. Maarten de Mol
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marko van Eekelen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Rinus Plasmeijer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Laboratory, Ericsson, P.O. Box 1505, 125 25, Älvsjö, Sweden

    Thomas Arts

  2. Lehrstuhl für Informatik II, RWTH Aachen, Ahornstr. 55, 52056, Aachen, Germany

    Markus Mohnen

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

de Mol, M., van Eekelen, M., Plasmeijer, R. (2002). Theorem Proving for Functional Programmers. In: Arts, T., Mohnen, M. (eds) Implementation of Functional Languages. IFL 2001. Lecture Notes in Computer Science, vol 2312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46028-4_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-46028-4_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43537-2

  • Online ISBN: 978-3-540-46028-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation