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.
Keywords for this software
References in zbMATH (referenced in 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
- Gerdes, Alex; Heeren, Bastiaan; Jeuring, Johan; van Binsbergen, L. Thomas: Ask-elle: an adaptable programming tutor for Haskell giving automated feedback (2017) MathEduc
- Achten, Peter; van Eekelen, Marko; de Mol, Maarten; Plasmeijer, Rinus: EditorArrow: an arrow-based model for editor-based programming (2013)
- de Mol, Maarten; van Eekelen, Marko: Beautiful code, beautiful proof? (2013)
- Tejfel, M.; Kozsik, T.; Horváth, Z.: A semantic model for proving properties of clean object I/O programs (2009)
- de Mol, Maarten; van Eekelen, Marko; Plasmeijer, Rinus: Proving properties of lazy functional programs with Sparkle (2008)
- van Eekelen, Marko; de Mol, Maarten: Proof tool support for explicit strictness (2006)
- Dowse, Malcolm; Butterfield, Andrew; van Eekelen, Marko: Reasoning about deterministic concurrent functional I/O (2005)
- Achten, Peter; van Eekelen, Marko; Plasmeijer, Rinus: Generic graphical user interfaces (2004)
- Kahl, Wolfram: Basic pattern matching calculi: a fresh view on matching failure (2004)
- 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: http://www.cs.ru.nl/~marko/research/sparkle/