Paper Info
Title
Theorem Proving for Functional Programmers
Abstract
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 different 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.
Year
DOI
Venue
2001
10.1007/3-540-46028-4_4
IFL
Keywords
Field
DocType
trivial goal,theorem proving,lazy graph-rewriting,difficult goal,different concept,larger program,small example proof,automated reasoning,functional programmers,new theorem prover,functional programming language,theorem prover,graph rewriting
Automated reasoning,Programming language,Functional programming,Computer science,Automated theorem proving,Theoretical computer science,Semantics
Conference
ISBN
Citations 
PageRank 
3-540-43537-9
27
1.45
References 
Authors
5
3
Name
Order
Citations
PageRank
Maarten de Mol11198.29
marko c j d van eekelen223930.37
Marinus J. Plasmeijer321023.72