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...

I think they also have an integration problem, ideally they would merge hs-to-coq with https://github.com/jwiegley/coq-haskell

They agree :-)

https://github.com/antalsz/hs-to-coq/issues/122

Last updated: Jun 25 2024 at 17:02 UTC