# A Calculus of Functional BSP Programs with Projection

Abstract : Bulk Synchronous Parallel ML (BSML) is an extension of the functional language Objective Caml to program Bulk Synchronous Parallel (BSP) algorithms. It is deterministic, deadlock free and performances are good and predictable. Parallelism is expressed with a set of 4 primitives on a parallel data structure called parallel vector. These primitives are pure functional ones: they have no side-effect. It is thus possible, and we did it, to prove the correctness of BSML programs using a proof assistant like Coq. The BS$\lambda$-calculus is an extension of the $\lambda$-calculus which models the core semantics of BSML. Nevertheless some principles of BSML are not well captured by this calculus. This paper presents a new calculus, with a projection primitive, which provides a better model of the core semantics of BSML.
Type de document :
Communication dans un congrès
International Parallel & Distributed Processing Symposium, 8th Workshop on Advances in Parallel and Distributed Computational Models, Apr 2006, Rhodes, Greece. IEEE Computer Society Press, 2006, 〈10.1109/IPDPS.2006.1639552〉

https://hal.inria.fr/inria-00452579
Contributeur : Frédéric Loulergue <>
Soumis le : mardi 2 février 2010 - 16:21:46
Dernière modification le : mercredi 29 novembre 2017 - 10:19:38

### Citation

Frédéric Loulergue. A Calculus of Functional BSP Programs with Projection. International Parallel & Distributed Processing Symposium, 8th Workshop on Advances in Parallel and Distributed Computational Models, Apr 2006, Rhodes, Greece. IEEE Computer Society Press, 2006, 〈10.1109/IPDPS.2006.1639552〉. 〈inria-00452579〉

### Métriques

Consultations de la notice