Bas Spitters (Aug 25 2020 at 16:10): Bas Spitters (Aug 25 2020 at 16:10):seems to be gaining some traction as a GHC plugin
https://ucsd-progsys.github.io/liquidhaskell-blog/2020/08/20/lh-as-a-ghc-plugin.lhs/
but hs-to-coq is easier to use. https://nikivazou.github.io/static/Haskell17/a-tale.pdf
It might be a way of slowly luring haskell programmers to Coq...
Karl Palmskog (Aug 25 2020 at 16:15):I think they also have an integration problem, ideally they would merge hs-to-coq with https://github.com/jwiegley/coq-haskell
Bas Spitters (Aug 25 2020 at 16:32):They agree :-)
https://github.com/antalsz/hs-to-coq/issues/122
Last updated: Apr 19 2024 at 21:01 UTC