Paper Info
Title
A Proof Tool Dedicated to Clean - The First Prototype
Abstract
Theorem proving for functional programming languages can be made much easier by the availability of a dedicated theorem prover. A theorem prover is dedicated to a specific programming language when it fully supports the syntax and semantics of the language and offers specialized proving support for it. Using a dedicated theorem prover is easy, because one can reason about a developed program without having to translate it. However, no suited dedicated theorem prover for a functional language exists yet. This paper describes a simple prototype of a dedicated theorem prover for the functional language Clean. A description of the possibilities of the prototype is given and an examination is made of the work that needs to be done to extend the prototype to a fully operational and truly useful programming tool. Also example proofs of some basic properties and of a graph transformation are given.
Year
Venue
Keywords
1999
AGTIVE
dedicated theorem prover,simple prototype,basic property,example proof,useful programming tool,functional language,proof tool,specific programming language,developed program,theorem prover,first prototype,functional programming language
Field
DocType
Volume
Functional programming,Computer science,Automated theorem proving,Theoretical computer science,Mathematical proof,Graph rewriting,Syntax,Semantics
Conference
1779
ISSN
ISBN
Citations 
0302-9743
3-540-67658-9
1
PageRank 
References 
Authors
0.59
2
2
Name
Order
Citations
PageRank
Maarten de Mol11198.29
marko c j d van eekelen223930.37