The blue social bookmark and publication sharing system.
Log in with your username.
I've lost my password.
Log in with your OpenID-Provider.
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.