Sciweavers

CEFP
2007
Springer

Proving Properties of Lazy Functional Programs with Sparkle

14 years 4 months ago
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...
Maarten de Mol, Marko C. J. D. van Eekelen, Rinus
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where CEFP
Authors Maarten de Mol, Marko C. J. D. van Eekelen, Rinus Plasmeijer
Comments (0)