Stream: hs-to-coq devs & users

Topic: verifying hs-to-coq itself


view this post on Zulip Quinn (Oct 22 2021 at 16:14):

How paranoid should I be that hs-to-coq itself isn't correct? Should we run hs-to-coq on the hs-to-coq source to validate properties of it?

view this post on Zulip Stephanie Weirich (Oct 22 2021 at 16:55):

This paper: https://www.seas.upenn.edu/~sweirich/papers/containers-jfp.pdf describes some of the testing that we have done with hs-to-coq to gain confidence in its correctness. Proving the system correct would be a significant undertaking.

view this post on Zulip Quinn (Oct 22 2021 at 17:47):

I see! the round trip testing suite correctness is exciting!


Last updated: Feb 06 2023 at 06:29 UTC