Skip to Main content Skip to Navigation
Conference papers

Parallel programming with Coq: Map and reduce skeletons on trees

Abstract : SyDPaCC is a set of libraries for the Coq interactive theorem prover. It allows to develop correct functional parallel programs on distributed lists based on the transformation of naive sequential programs that are considered as specifications. To offer the parallelization of functions on other data structures, the first step is to implement a parallel version of the considered data structure and to provide parallel implementations of primitive functions manipulating it. This paper presents such a first step: a binary tree extension which includes new map and reduce pure functional algorithmic skeletons for binary trees. Such algorithmic skeletons are templates of parallel algorithms, realized in a functional context as higher-order functions implemented in parallel. The use of these new primitives is illustrated on example applications.
Document type :
Conference papers
Complete list of metadata
Contributor : Frédéric Loulergue <>
Submitted on : Tuesday, October 15, 2019 - 6:24:15 PM
Last modification on : Monday, November 30, 2020 - 5:48:18 PM



Jolan Philippe, Frédéric Loulergue. Parallel programming with Coq: Map and reduce skeletons on trees. 34th ACM/SIGAPP Symposium on Applied Computing (SAC), Apr 2019, Limassol, Cyprus. pp.1578-1581, ⟨10.1145/3297280.3299742⟩. ⟨hal-02317074⟩



Record views