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 | <CALhYyxMfU1N+k+Mr7_eFZDzA5rPnF961HXTDA2ZZQmf-6h_QXw@mail.gmail.com> |
So far I've been reading https://www.cs.purdue.edu/homes/bendy/Fiat/FiatByteString.pdf. I'm interested in the ideas presented in https://github.com/DistributedComponents/verdi-runtime, which is OCaml based. My goal is to provide building blocks for verifying and testing Cloud Haskell programs. I've been looking at existing frameworks (such as quickcheck-state-machine/-distributed and hedgehog) for model based testing, and ways of injecting an application layer scheduler for detecting race conditions. The final bit of the puzzle is being able to apply formal methods to verify concurrent/distributed algorithms, and generate some (if not all) of the required implementation code. Any pointers to research or prior art would be greatly appreciated. Cheers, Tim Watson -- 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.