We address the correctness problem of parallel implementation of functional programs. Those functional programs are evaluated by a set of concurrent agents communicating with each other and cooperating together while the computations progress. New communications among agents are introduced to improve the performance, because properties or facts about functions to be computed are exploited. In particular we show that those communications may avoid redundant computations of intermediate results. We provide the logical theories for proving correctness of implementation of functional programs together with facts about those programs.