Sound rules for parallel evaluation of a functional language callcc
Luc Moreau, Daniel Ribbens · 1993
Observationally equivalent programs are programs which are indistinguishable in aJl contexts, aa far aa their termination property ie concerned.In this paper, we present rules preserving observational equivrdence, for the parallel evaluation of programs using call/cc.These rules idlow the capture of continuations in any applicative context and they prevent from aborting the whole computation when a continuation is applied in the extent of the call/cc by which it was reified.As a consequence, these results prove that one can design a functional language with first-class continuations which haa transparent constructs for parallelism.