11
$\begingroup$

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?

Improve this question
$\endgroup$
0

4 Answers 4

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thank you! Sure, if I find more ressources, I will make sure to add them to my post. $\endgroup$
    – FK82
    Commented Sep 12, 2016 at 16:27
6
$\begingroup$

You can start with

Topics include basic concepts of logic, computer-assisted theorem proving, the Coq proof assistant, functional programming, operational semantics, Hoare logic, and static type systems. The exposition is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers. No specific background in logic or programming languages is assumed, though a degree of mathematical maturity will be helpful.

You can skip (or skim) the programming language theory parts and only learn how to deal with formal proofs starting from Preface up to IndPrinciples. The book is really well-written and illuminating.

Then you might want to proceed with

In this volume you will learn how to specify and verify (prove the correctness of) sorting algorithms, binary search trees, balanced binary search trees, and priority queues. Before using this book, you should have some understanding of these algorithms and data structures, available in any standard undergraduate algorithms textbook. You should understand all the material in Software Foundations Volume 1 (Logic Foundations)

A note of warning: VFA is still in beta-release!

Improve this answer
$\endgroup$
10
  • $\begingroup$ (Your second link directs to the wrong place.) Also, there is Verified Functional Programming in Agda; which uses Agda, formally a programming language but uses unicode and so is closer to math notation. $\endgroup$
    – Musa Al-hassy
    Commented Sep 14, 2016 at 14:57
  • $\begingroup$ Corrected, thanks. Yes, I've read VFPiA, but it is not to my taste. $\endgroup$
    – Anton Trunov
    Commented Sep 14, 2016 at 17:11
  • $\begingroup$ Thank you for your answer! I think there is a misconception. I'm not looking for functional techniques for proving algorithms (such as a proof assistant), but for techniques for proving functional code (for example for proving a functional implementation of a given algorithm correct) @MusaAl-hassy answer is very close to my desired answer. In case I missed it and the books you cited cover this aspect as well, would you mind adding the relevant chapters? $\endgroup$
    – FK82
    Commented Sep 17, 2016 at 14:22
  • $\begingroup$ @FK82 Here is a Theorem app_assoc : ∀ l1 l2 l3 : natlist, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3) from the Lists chapter. Does this example look anything like the thing you're interested in? They start with functional programming in Coq, but then move on to reasoning about the properties of functional programs. The chapters from Preface up to IndPrinciples cover both of those, and I'd say programming and reasoning are intertwined there. $\endgroup$
    – Anton Trunov
    Commented Sep 17, 2016 at 15:34
  • 1
    $\begingroup$ @FK82 (1) I totally agree with this comment. (2) You might want to look at the book "Thinking Functionally with Haskell" (2015) by R. Bird. The book has tons of examples of reasoning about Haskell. (3) Also, "Pearls of Functional Algorithm Design" (2010) by the same author may be of some help to you. $\endgroup$
    – Anton Trunov
    Commented Sep 18, 2016 at 15:38
5
$\begingroup$

It turns out that an excellent source of proof techniques and examples for proving things about pure functional languages is proof assistants which usually include as part of their specification language a pure functional language on which it is possible to reason equationally.

One might want to consult a book like Certified Programing with Dependent Types for an in-depth introduction to this kind of reasoning in a specific proof assistant, namely Coq.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Thanks! I'm actually looking specifically for techniques in Haskell. My post was edited to include all functional code, but that's well above my intentions. $\endgroup$
    – FK82
    Commented Sep 17, 2016 at 14:25
  • 1
    $\begingroup$ I'm not aware of systems designed to verify Haskell specifically, but I would note that 1) The functional core of Coq (and Agda) is essentially indistinguishable from that of Haskell (except for the restriction to total functions) and 2) Programs verified in Coq and Agda can be extracted to Haskell (though I believe extraction to Haskell is better supported in Agda, where Coq is more Ocaml-centric) $\endgroup$
    – cody
    Commented Sep 18, 2016 at 13:13
  • $\begingroup$ Good to know! This would however imply that I rewrite my program (or the relevant parts) in Coq or Agda. I don't think that's reasonable in my case. $\endgroup$
    – FK82
    Commented Sep 19, 2016 at 13:40
  • $\begingroup$ There are a couple of very experimental "front ends" that try to convert Haskell to Isabelle or directly prove equivalences using Isabelle, but I wouldn't hold too much stock in their maturity. I think re-writing the code would ultimately be less work. $\endgroup$
    – cody
    Commented Sep 19, 2016 at 15:37
4
$\begingroup$

I suggest to use program logics. They deal much better with effects than typing systems.

There are numerous program logics for functional languages. This becomes interesting with effects. See e.g. Logical Reasoning for Higher-Order Functions with Local State.

Work by Arthur Charguéraud integrates the program logic approach with proof assistants, see e.g. this overview page.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.