In Javascript understanding functional programming is becoming a necessity to quickly on-board and become productive thanks to React and Flux. But with Monad and Setoid groups, being able to grok FP…
We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end,we present a tool, named hs-to-coq, that translates total Haskell programs into Coq programs via a shallow embedding.