Does anyone have much experience generating Haskell from Coq?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Does anyone have much experience generating Haskell from Coq?

Tim Watson
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 


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: [cloud-haskell-developers] Does anyone have much experience generating Haskell from Coq?

Gershom Bazerman
The other approach, which has been quite successful, by the penn team,
is using hs-to-coq to extract coq from haskell and _then_ verify:
https://github.com/antalsz/hs-to-coq

-g
On Sat, Dec 8, 2018 at 7:05 AM Tim Watson <[hidden email]> wrote:

>
> 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
>
> --
>
>
>
> Visit this group at https://groups.google.com/group/cloud-haskell-developers.
>
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: [cloud-haskell-developers] Does anyone have much experience generating Haskell from Coq?

Tim Watson
On Mon, 10 Dec 2018, 09:30 Gershom B <[hidden email] wrote:
The other approach, which has been quite successful, by the penn team,
is using hs-to-coq to extract coq from haskell and _then_ verify:
https://github.com/antalsz/hs-to-coq

Thank you! Someone else proposed that off list yesterday too. If we get our layering right, that could definitely be a viable alternative!

I will do some more research. I generally think that https://deepspec.org/ is an awesome idea. :) 



_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users