Clever Geek Handbook

Is there a translator from Haskell to Kok?

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

There seem to be tools to translate OCaml programs. But what about Haskell?

+3


source to share


1 answer


The main problem I see with this kind of translation is that Haskell programs (as well as Ocaml) can execute any recursion algorithm and can contain loops.

Coq doesn't have a built-in notion of loops, and any recursive function must end and be explicit about why it ends.



As far as I know, there is no such tool at the moment.

+4


source






More articles:


All Articles