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.
I now have a similar use case and would like to run extracted code on a cluster. Any experience with this?
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