Skip to main content
SpringerLink
Log in

Proving Properties of Lazy Functional Programs with Sparkle

  • Chapter
Central European Functional Programming School (CEFP 2007)

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

Included in the following conference series:

Abstract

This tutorial paper aims to provide the necessary expertise for working with the proof assistant Sparkle, which is dedicated to the lazy functional programming language Clean. The purpose of a proof assistant is to use formal reasoning to verify the correctness of a computer program. Formal reasoning is very powerful, but is unfortunately also difficult to carry out.

Due to their mathematical nature, functional programming languages are well suited for formal reasoning. Moreover, Sparkle offers specialized support for reasoning about Clean, and is integrated into its official development environment. These factors make Sparkle a proof assistant that is relatively easy to use.

This paper provides both theoretical background for formal reasoning, and detailed information about using Sparkle in practice. Special attention will be given to specific aspects that arise due to lazy evaluation and due to the existence of strictness annotations. Several assignments are included in the text, which provide hands-on experience with Sparkle.

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 69.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

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. Abel, A., Benke, M., Bove, A., Hughes, J., Norell, U.: Verifying Haskell programs using constructive type theory. In: Leijen, D. (ed.) Proceedings of the ACM SIGPLAN 2005 Haskell Workshop, Tallinn, Estonia, pp. 62–74. ACM Press, New York (2005)

    Chapter  Google Scholar 

  2. Barendregt, H.P., van Eekelen, M.C.J.D., Glauert, J.R.W., Kennaway, R., Plasmeijer, M.J., Sleep, M.R.: Term graph rewriting. In: de Bakker, J.W., Nijman, A.J., Treleaven, P.C. (eds.) PARLE 1987. LNCS, vol. 259, pp. 141–158. Springer, Heidelberg (1987)

    Google Scholar 

  3. Barendsen, E., Smetsers, S.: Graph rewriting aspects of functional programming. In: Handbook of Graph Grammars and Computing by Graph Transformation, pp. 63–102. World Scientific, Singapore (1999)

    Google Scholar 

  4. Bird, R.S.: Introduction to Functional Programming using Haskell, 2nd edn. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  5. Brus, T.H., van Eekelen, M.C.J.D., van Leer, M.O., Plasmeijer, M.J.: Clean: A language for functional graph writing. In: Proceedings of the Functional Programming Languages and Computer Architecture, pp. 364–384. Springer, Heidelberg (1987)

    Google Scholar 

  6. Burn, G.L.: Evaluation transformers a model for the parallel evolution of functional languages. In: Proc. of a conference on Functional programming languages and computer architecture, pp. 446–470. Springer, Heidelberg (1987)

    Google Scholar 

  7. Butterfield, A., Strong, G.: Proving Correctness of Programs with I/O - a paradigm comparison. In: Arts, T., Mohnen, M. (eds.) IFL 2002. LNCS, vol. 2312, pp. 72–88. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Butterfield, A., Strong, G.: Proving correctness of programs with io - a paradigm comparison. In: Arts, T., Mohnen, M. (eds.) IFL 2002. LNCS, vol. 2312, pp. 72–87. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  9. Coquand, T., Dybjer, P., Hughes, J., Sheeran, M.: Combining verification methods in software development. Project proposal, Chalmers Institute of Techology, Sweden (December 2001)

    Google Scholar 

  10. Danielsson, N.A., Hughes, J., Jansson, P., Gibbons, J.: Fast and loose reasoning is morally correct. SIGPLAN Not. 41(1), 206–217 (2006)

    Article  Google Scholar 

  11. de Mol, M., van Eekelen, M., Plasmeijer, R.: Theorem proving for functional programmers - Sparkle: A functional theorem prover. In: Arts, T., Mohnen, M. (eds.) IFL 2002. LNCS, vol. 2312, pp. 55–72. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  12. de Mol, M., van Eekelen, M., Plasmeijer, R.: A single-step term-graph reduction system for proof assistants. In: Schürr, A., Nagl, M., Zündorf, A. (eds.) Proceedings of Selected and Invited Papers of Applications of Graph Transformations with Industrial Relevance, Third International Symposium, AGTIVE 2007, Kassel, Germany, pp. 181–197 (2007)

    Google Scholar 

  13. de Mol, M., van Eekelen, M., Plasmeijer, R.: The Mathematical Foundation of the Proof Assistant Sparkle. Technical Report ICIS–R07025, Radboud University Nijmegen (November 2007)

    Google Scholar 

  14. Dowse, M., Butterfield, A., van Eekelen, M.C.J.D.: Reasoning About Deterministic Concurrent Functional I/O. In: Grelck, C., Huch, F., Michaelson, G., Trinder, P.W. (eds.) IFL 2004. LNCS, vol. 3474, pp. 177–194. Springer, Heidelberg (2004)

    Google Scholar 

  15. Gill, A.: The technology behind a graphical user interface for an equational reasoning assistant. In: Turner, D.N. (ed.) Functional Programming. Workshops in Computing, p. 4. Springer, Heidelberg (1995)

    Google Scholar 

  16. Gill, A.: Introducing the haskell equational reasoning assistant. In: Haskell 2006: Proceedings of the 2006 ACM SIGPLAN workshop on Haskell, pp. 108–109. ACM Press, New York (2006)

    Chapter  Google Scholar 

  17. Gordon, A.: Bisimilarity as a theory of functional programming. In: Proceedings of the Eleventh Conference on the Mathematical Foundations of Programming Semantics. Electronic Notes in Theoretical Computer Science, vol. 1. Elsevier Science B.V, Amsterdam (1995)

    Google Scholar 

  18. Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF. LNCS, vol. 78. Springer, Berlin (1979)

    Google Scholar 

  19. Horváth, Z., Kozsik, T., Tejfel, M.: Proving invariants of functional programs. In: Kilpeläinen, P., Päivinen, N. (eds.) SPLST. Department of Computer Science, pp. 115–126. University of Kuopio (2003)

    Google Scholar 

  20. Hudak, P., Jones, S.L.P., Wadler, P., Boutel, B., Fairbairn, J., Fasel, J.H., Guzmán, M.M., Hammond, K., Hughes, J., Johnsson, T., Kieburtz, R.B., Nikhil, R.S., Partain, W., Peterson, J.: Report on the Programming Language Haskell, A Non-strict, Purely Functional Language. SIGPLAN Notices 27(5), R1–R164 (1992)

    Google Scholar 

  21. van Kesteren, R., van Eekelen, M., de Mol, M.: Proof support for general type classes. In: Loidl, H.-W. (ed.) Trends in Functional Programming 5: Selected papers from the Fifth International Symposium on Trends in Functional Programming, TFP 2004, München, Germany, Intellect, pp. 1–16 (2004)

    Google Scholar 

  22. Mintchev, S.: Mechanized reasoning about functional programs. In: Hammond, K., Turner, D., Sansom, P. (eds.) Proceedings of the Glasgow Functional Progamming Workshop, pp. 151–167. Springer, Heidelberg (1994)

    Google Scholar 

  23. Noll, T., Fredlund, L., Gurov, D.: The evt erlang verification tool. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 582–585. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  24. Owre, S., Shankar, N., Rushby, J., Stringer-Calvert, D.: PVS Language Reference (version 2.4) (2001), http://pvs.csl.sri.com/doc/pvs-prover-guide.pdf

  25. Paulson, L.C.: Logic and Computation. Cambridge University Press, Cambridge (1987)

    MATH  Google Scholar 

  26. Paulson, L.C.: The Isabelle Reference Manual. University of Cambridge (2007), http://isabelle.in.tum.de/doc/ref.pdf

  27. Plasmeijer, R., van Eekelen, M.: Functional Programming and Parallel Graph Rewriting. Addison-Wesley Publishing Company, Reading (1993)

    MATH  Google Scholar 

  28. Plasmeijer, R., van Eekelen, M.: Keep it clean: a unique approach to functional programming. SIGPLAN Not. 34(6), 23–31 (1999)

    Article  Google Scholar 

  29. Plasmeijer, R., van Eekelen, M.: Concurrent CLEAN Language Report (version 2.0) (December 2001), http://www.cs.ru.nl/~clean/

  30. Tejfel, M., Horváth, Z., Kozsik, T.: Extending the sparkle core language with object abstraction. Acta Cybern. 17(2) (2006)

    Google Scholar 

  31. The Coq Development Team. The Coq Proof Assistant Reference Manual (version 7.3). Inria (2002), http://pauillac.inria.fr/cdrom/www/coq/doc/main.html

  32. Trinder, P.W., Hammond, K., Loidl, H.-W., Jones, S.L.P.: Algorithm + strategy = parallelism. J. Funct. Program. 8(1), 23–60 (1998)

    Article  MATH  Google Scholar 

  33. van Eekelen, M., de Mol, M.: Proof tool support for explicit strictness. In: Butterfield, A., Grelck, C., Huch, F. (eds.) IFL 2005. LNCS, vol. 4015, pp. 37–54. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  34. Winstanley, N.: Era User Manual, version 2.0. University of Glasgow (March 1998), http://www.dcs.gla.ac.uk/~nww/Era/Era.html

Download references

Author information

Authors and Affiliations

  1. Institute for Computing and Information Sciences, Radboud University 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. Dept. of Programming Languages and Compilers, Hungary

    Zoltán Horváth

  2. Radboud Universiteit Nijmegen, Netherlands

    Rinus Plasmeijer

  3. BabeÅŸ-Bolyai University, 400084, Cluj-Napoca, Romania

    Anna Soós

  4. Faculty of Informatics, Eötvös Loránd University, 1117, Budapest, Hungary

    Viktória Zsók

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

de Mol, M., van Eekelen, M., Plasmeijer, R. (2008). Proving Properties of Lazy Functional Programs with Sparkle . In: Horváth, Z., Plasmeijer, R., Soós, A., Zsók, V. (eds) Central European Functional Programming School. CEFP 2007. Lecture Notes in Computer Science, vol 5161. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88059-2_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-88059-2_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-88058-5

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation