Re: [cloud-haskell-developers] Does anyone have much experience generating Haskell from Coq?
Tim Watson <[email protected]>
| Newsgroups | gmane.comp.lang.haskell.parallel,gmane.comp.lang.haskell.glasgow.user |
|---|---|
| Message-ID | <CALhYyxOWP+OMWGpsFGLpSREyFLMw=pvcidZ9JR1k=sBDezu5iA@mail.gmail.com> |
On Mon, 10 Dec 2018, 09:30 Gershom B <[email protected] wrote: > The other approach, which has been quite successful, by the penn team, > is using hs-to-coq to extract coq from haskell and _then_ verify: > https://github.com/antalsz/hs-to-coq Thank you! Someone else proposed that off list yesterday too. If we get our layering right, that could definitely be a viable alternative! I will do some more research. I generally think that https://deepspec.org/ is an awesome idea. :) -- You received this message because you are subscribed to the Google Groups "parallel-haskell" group. To unsubscribe from this group and stop receiving emails from it, send an email to parallel-haskell+unsubscribe-/JYPxA39Uh5TLH3MbocFF+G/[email protected] For more options, visit https://groups.google.com/d/optout.