This page intends to collect information, documentation and publications on Sparkle, the dedicated proof-assistant of the lazy functional programming language Clean.

1. The Sparkle Version to be used at the Central European Functional Programming Summer School 2007.

2. The answers for the assignments of the Sparkle course of CEFP 2007.

3. The revised lecture notes for the Sparkle course of CEFP 2007.

4. The draft lecture notes for the Sparkle course of CEFP 2007.

5. Maarten de Mol's page on sparkle: Sparkle's main page at Nijmegen University, Nijmegen, The Netherlands.

6. Malcolm Dowse's documentation on Sparkle at Trinity College, Dublin, Ireland.

7. Andy Fugard's documentation on Sparkle at Chalmers University, Göteborg, Sweden.

8. Maarten de Mol, Marko van Eekelen, Rinus Plasmeijer. The Mathematical Foundation of Sparkle. Technical Report ICIS-R07025. Radboud University Nijmegen. November 2007.

9. Maarten de Mol, Marko van Eekelen, Rinus Plasmeijer. Confluent Term-Graph Reduction for Computer-Aided Formal Reasoning. Technical Report ICIS-R07012. Radboud University Nijmegen. May 2007.

10. Peter Achten, Marko van Eekelen, Maarten de Mol, Rinus Plasmeijer. An Arrow Based Semantics for Interactive Applications. In Marco Morazán and Henrik Nillsson (eds). Proceedings of the Eighth Symposium on Trends in Functional Programming, TFP 2007, New York City, USA, 2-4 april 2007. pp IX-1-16, Seton Hall University. TR-SHU-CS-2007-04-1.

11. Peter Achten, Marko van Eekelen, Rinus Plasmeijer. Towards A Unified Semantic Model For Interactive Applications Using Arrows And Generic Editors. In Henrik Nillsson (ed). Proceedings of the Seventh Symposium on Trends in Functional Programming, TFP 2006, Nottingham, UK, 19-21 april 2006. pp 279-292, University of Nottingham.

12. Marko van Eekelen, Maarten de Mol. Proof Tool Support for Explicit Strictness Proof Tool Support for Explicit Strictness. Selected Papers of the 17^th International Workshop Proceedings of Implementation and Application of Functional Languages, IFL'05, Dublin, Ireland, IFL 2005, LNCS 4015, pp 37-54.

13. Peter Achten, Marko van Eekelen, Rinus Plasmeijer. A Unified Semantic Model For Interactive Applications Using IData And Generic Editors (abstract). In Zoltan Horvath, Viktoria Zsok (eds) Proceedings of the 18th Symposium on Implementation and Application of Functional Programming, IFL 2006, Budapest, Hungary, Sept. 4-6 2006. Technical Report 2006-S01, ISBN 9634638767. pp 205.

14. Marko van Eekelen, Maarten de Mol. Effects of Changing Strictness Properties (abstract). In Implementation and Application of Functional Languages. 17^th International Workshop, IFL’05. Andrew Butterfield (ed.), Dublin, 2005. Technical Report TCD-CS-2005-60, Trinity College Dublin.

15. Ron van Kesteren, Marko van Eekelen, Maarten de Mol. Proof Support for General Type Classes, Trends in Functional Programming Volume 5, Selected papers from the Fifth Symposium on Trends in Functional Programming (TFP 2004), editor Hans Wolfgang Loidl. Intellect Publishers, pp 1-16.
This paper received by unanimous vote the Best Student Paper Award of TFP04.

16. HORVÁTH Zoltán, KOZSIK Tamás, TEJFEL Máté: Verifying invariants of abstract functional objects - a case study. In: Proceedings of 6th International Conference on Applied Informatics (ICAI'04), Eger, Hungary, 2004. pdf.

17. Ron van Kesteren, Marko van Eekelen, Maarten de Mol. An Effective Proof Rule for General Type Classes. Proc. of the Fifth Symposium on Trends in Functional Programming (TFP 2004), editor Hans Wolfgang Loidl, November 2004, München, pp 149-165, Ludwig Maximilians Universität München. Abstract.

18. Leonard Lensink, Marko van Eekelen. Induction and Co-induction in Sparkle. Proc. of the Fifth Symposium on Trends in Functional Programming (TFP 2004), editor Hans Wolfgang Loidl, November 2004, München, pp 273-295, Ludwig Maximilians Universität München. Abstract.

19. Malcolm Dowse, Andrew Butterfield, Marko van Eekelen, A Language for Reasoning about Concurrent Functional I/O. Selected Papers of the 16^th International Workshop Proceedings of Implementation and Application of Functional Languages, IFL'04, Lübeck, Germany, IFL 2004, LNCS 3074, pp 177-195. Abstract.

20. Maarten de Mol, Marko van Eekelen, Rinus Plasmeijer. Theorem Proving for Functional Programmers - SPARKLE: A Functional Theorem Prover. In: Arts, Th., Mohnen M., eds. Proceedings of the 13th International Workshop on the Implementation of Functional Languages, IFL 2001, Selected Papers, Älvsjö, Sweden, September 24-26, 2001, Springer-Verlag, LNCS 2312, pages 55-71. abstract, pdf.

21. Malcolm Dowse, Andrew Butterfield, Marko van Eekelen, Maarten de Mol, Rinus Plasmeijer. Towards Machine-Verified Proofs for I/O. Grelck, C., Huch, F. Eds. Proceedings Implementation and Application of Functional Languages, 16th International Workshop, IFL'04, Lübeck, Germany, September 8-10, 2004, Technical Report 0408, Christian-Albrechts-Universität zu Kiel, pp. 469-480. This paper also appeared as NIII Technical Report 0415. The Sparkle proofs of this NIII TR0415 report can still be downloaded.

22. Marko van Eekelen, Maarten de Mol. Mixed Lazy/Strict Graph Semantics. Grelck, C., Huch, F. Eds. Proceedings Implementation and Application of Functional Languages, 16th International Workshop, IFL'04, Luebeck, Germany, September 8-10, 2004, Technical Report 0408, Christian-Albrechts-Universität zu Kiel, pp.245-260.

23. Marko van Eekelen and Maarten de Mol. Reasoning about explicit strictness in a lazy language using mixed lazy/strict semantics. In: Peña, R. ed. Proceedings of the 14th International Workshop on the Implementation of Functional Languages, IFL 2002, Madrid, Spain, September 16-18, 2002, Technical Report 127-02, Departamento de Sistemas Informáticos y Programación, Universidad Complutense de Madrid, pages 357-373. abstract, pdf.

24. Maarten de Mol, Marko van Eekelen, and Rinus Plasmeijer. Theorem Proving for Functional Programmers. In: Arts, Th., Mohnen, M. eds. Proceedings of the 13th International workshop on the Implementation of Functional Languages, IFL'01, Älvsjö, Sweden, September 24-26, 2001, Ericsson Computer Science Laboratory, pp.99-118. powerpoint presentation

25. Agtive paper….