I want to provide proofs for parts of a Haskell program I'm writing as part of my thesis. So far however, I failed to find a good reference work.
Graham Hutton's introductory book Programming in Haskell (Google Books)—which I read while learning Haskell—touches on a few techniques for reasoning about programs such as
- equational reasoning
- using non-overlapping patterns
- list induction
in chapter 13 but it's not very in-depth.
Are there any books or article you can recommend which provide a more detailed overview of formal proving techniques for Haskell, or other functional, code?
Asked By : FK82
Answered By : Musa Al-hassy
One of the de facto methods for proving results in functional programming is via Richard Bird's group.
In particular, you ask for an in-depth or at least more comprehensive approach to equational reasoning and list induction and this is provided in Lectures on Constructive Functional Programming.
More generally, the text "Algebra of Programming", by Bird and de Moor, also deals with the correctness of functional algorithms such as optimisation and dynamic programming problems.
If you come across other useful resources for this problem, please mention them and perhaps we can turn this post into a wiki.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/63363
0 comments:
Post a Comment
Let us know your responses and feedback