Correctness of Non-determinism Analyses in a Parallel-Functional Language