4

If I want to write proofs and algorithms/semantics using Coq on a Haskell program. How can I translate from Haskell to Coq to do this?

It seems that there are tools to translate OCaml programs. But how about Haskell?

xywang
  • 941
  • 8
  • 24
  • 5
    Somewhat relevant: you can definitely go [the other direction](http://stackoverflow.com/questions/13334863/can-i-extract-a-coq-proof-as-a-haskell-function). – Cactus Jul 09 '15 at 01:39
  • This isn't an answer to the question, but you might also be interested in HERMIT. It is a toolkit for proving theorems about Haskell code (among other things). If you do decide to check it out I would suggest looking at HERMIT-shell, which is the new (and currently under active development) shell for the system. Full disclosure: I work on HERMIT and HERMIT-shell as part of my job. – David Young Jul 09 '15 at 02:57
  • @DavidYoung Can HERMIT help to prove arbitrary property or just optimized code equivalence? The short introduction seems to indicate the latter one. – xywang Jul 09 '15 at 03:01
  • @xywang You can use it to prove properties of a Haskell program, too. There are examples of this in the examples/laws directory. Here is the HERMIT-shell version: https://github.com/ku-fpg/hermit-shell/tree/master/examples/laws. The Haskell file "under scrutiny" here is `ListLaws.hs` and the other files are HERMIT-shell script files (also written in Haskell, using the HERMIT-shell DSL) that prove theorems about the code in the `ListLaws.hs` file. The GHC `RULES` get turned into lemmas, which can then be proven. – David Young Jul 09 '15 at 03:09
  • [coq-haskell](https://github.com/jwiegley/coq-haskell) might also be relevant – Cactus Jul 10 '15 at 02:29
  • 5
    Perhaps this belongs at softwarerecs.stackexchange.com - New info about it though, Antal Spector-Zabusky posted software project [hs-to-coq](https://github.com/antalsz/ha-to-coq) "in fairly good shape", funded under a grant NSF 1521602 ["DeepSpec"](http://DeepSpec.org) with principal investigator Andrew Appel at Princeton University. – minopret Apr 28 '17 at 14:53

1 Answers1

5

The main issue I see in such a translation is that Haskell programs (as well as Ocaml ones) can perform any kind of recursion algorithm, and might contain loops.

In Coq, there is no build-in notion of loops, and any recursive function has to terminate, and be explicit why it terminates.

To the best of my knowledge, there is no such tool at the moment.

Vinz
  • 5,997
  • 1
  • 31
  • 52
  • 1
    There is a paper that describes a method for [converting "total functional programs"](https://www.cis.upenn.edu/~criz/publications/hs_to_coq.pdf) from Haskell into Coq. – Anderson Green Feb 07 '19 at 23:05