Parallel programming with Coq: Map and reduce skeletons on trees - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

Parallel programming with Coq: Map and reduce skeletons on trees

Résumé

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.
Fichier non déposé

Dates et versions

hal-02317074 , version 1 (15-10-2019)

Identifiants

Citer

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⟩
50 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More