Proving Properties of Lazy Functional Programs with Sparkle

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, w...

• Type: Conference
• Year: 2007
• Where: CEFP
• Authors: Maarten de Mol, Marko C. J. D. van Eekelen, Rinus Plasmeijer
• Keywords: CEFP 2007, Formal Reasoning, Functional Programming Languages, Programming Languages, Proof Assistant