Theorem Proving for Functional Programmers. 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.

References in zbMATH (referenced in 14 articles , 1 standard article )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Gerdes, Alex; Heeren, Bastiaan; Jeuring, Johan; van Binsbergen, L. Thomas: Ask-elle: an adaptable programming tutor for Haskell giving automated feedback (2017) MathEduc
  2. Achten, Peter; van Eekelen, Marko; de Mol, Maarten; Plasmeijer, Rinus: EditorArrow: an arrow-based model for editor-based programming (2013)
  3. de Mol, Maarten; van Eekelen, Marko: Beautiful code, beautiful proof? (2013) ioport
  4. Tejfel, Máté: Proving composed specifications of Clean programs in Sparkle-T (2009)
  5. Tejfel, M.; Kozsik, T.; Horváth, Z.: A semantic model for proving properties of clean object I/O programs (2009)
  6. de Mol, Maarten; van Eekelen, Marko; Plasmeijer, Rinus: Proving properties of lazy functional programs with Sparkle (2008)
  7. Kieburtz, Richard B.: Programmed strategies for program verification (2007)
  8. Tejfel, Máté; Horváth, Zoltán; Kozsik, Tamás: Temporal properties of Clean programs proven in Sparkle-T (2006)
  9. van Eekelen, Marko; de Mol, Maarten: Proof tool support for explicit strictness (2006)
  10. Dowse, Malcolm; Butterfield, Andrew; van Eekelen, Marko: Reasoning about deterministic concurrent functional I/O (2005)
  11. Tejfel, Máté; Horváth, Zoltán; Kozsik, Tamás: Extending the sparkle core language with object abstraction (2005)
  12. Achten, Peter; van Eekelen, Marko; Plasmeijer, Rinus: Generic graphical user interfaces (2004)
  13. Kahl, Wolfram: Basic pattern matching calculi: a fresh view on matching failure (2004)
  14. de Mol, Maarten; van Eekelen, Marko; Plasmeijer, Rinus: Theorem proving for functional programmers. SPARKLE: a functional theorem prover (2002)

Further publications can be found at: