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 Haskelltouches on a few techniques for reasoning about programs such asequational reasoningusing non-overlapping patternslist inductionin 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?
What are common formal techniques for proving functional code correct?
reference request;proof techniques;functional programming;books;program verification
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.