Stream: Coq users

Topic: Extracting to parallel computation


view this post on Zulip Bas Spitters (Aug 19 2020 at 13:34):

A decade ago we extracted our implementation of the Riemann integral to haskell and used the par/seq operations in Coq to get an easy 3x speedup on a 4 core machine. http://arxiv.org/abs/0809.1552
I now have a similar use case and would like to run extracted code on a cluster. Any experience with this?
This https://ocamlverse.github.io/content/parallelism.html
suggests targeting either parmap or parallel-for, of course, we could also use par/seq in haskell as before.
I'm just curious whether others have tried this.


Last updated: Sep 25 2023 at 12:01 UTC