Paper Info
Title
A Proof Tool for Reasoning About Functional Programs
Abstract
. This paper describes a system to support reasoning aboutlazy functional programs. We describe an approach based on combininga deep embedding of the language in HOL and a set of proof tools to raisethe level of interaction with the theorem prover. This approach allowsmeta-theoretic reasoning about the semantics and reasoning about undefinedprograms while still supporting practical reasoning about programsin the language.1 IntroductionIt is often claimed that functional programming...
Year
DOI
Venue
1996
10.1007/BFb0105400
TPHOLs
Keywords
Field
DocType
proof tool,functional programs,theorem prover,functional programming,practical reasoning
HOL,Computer-assisted proof,Embedding,Practical reason,Computer science,Automated theorem proving,Algorithm,Theoretical computer science,Deductive reasoning,Reasoning system,Semantics
Conference
ISBN
Citations 
PageRank 
3-540-61587-3
5
0.52
References 
Authors
11
1
Name
Order
Citations
PageRank
Graham Collins1726.19