search

antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

coq-haskell ? #122

Closed spitters closed 5 years ago

spitters commented 5 years ago

Is there (a planned) interaction between coq-haskell and hs-to-coq? https://github.com/jwiegley/coq-haskell

by @jwiegley

It seems like your structural-isomorphism-plugin may try to do something like that, but it's not documented.

sweirich commented 5 years ago

We have no current plans to integrate these projects (beyond the experience that John has already contributed to the creation of the base library: https://github.com/antalsz/hs-to-coq/tree/master/base).

spitters commented 5 years ago

Thanks. I made a link in the stdlib2 discussion. I'm wondering how/whether we would like to connect the haskell specific development with the corresponding idiomatic Coq development. Parametricity, as in CoqEAL, comes to mind.

jwiegley commented 5 years ago

If anything, coq-haskell ought to become an ever-thinner wrapper around hs-to-coq's base library, since hs-to-coq represents a more faithful encoding of the Haskell libraries I'm trying to mimick.