https://hal.inria.fr/hal-02317074Philippe, JolanJolanPhilippeNorthern Arizona University [Flagstaff]Loulergue, FrédéricFrédéricLoulergueNorthern Arizona University [Flagstaff]LIFO - Laboratoire d'Informatique Fondamentale d'Orléans - UO - Université d'Orléans - INSA CVL - Institut National des Sciences Appliquées - Centre Val de Loire - INSA - Institut National des Sciences AppliquéesParallel programming with Coq: Map and reduce skeletons on treesHAL CCSD2019[INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]Loulergue, Frédéric2019-10-15 18:24:152022-01-18 17:44:012019-10-15 18:24:15enConference papers10.1145/3297280.32997421SyDPaCC 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.