An extension of the -calculus called BS is introduced as a formal basis for functional languages expressing bulk synchronous parallel algorithms. A con uence result is shown. The application of the calculus is illustrated by examples of program proofs and the associated notion of parallel reduction. The reduction process is interpreted in the BSP cost model. c 2000 Elsevier Science B.V. All rights reserved.