Calculating Parallel Programs in Coq using List Homomorphisms

Frédéric Loulergue 1, 2, 3 Wadoud Bousdira 1, 2 Julien Tesson 4
3 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
Abstract : SyDPaCC is a set of libraries for the Coq proof assistant. It allows to write naive functional programs (i.e. with high complexity) that are considered as specifications, and to transform them into more efficient versions. These more efficient versions can then be automatically parallelised before being extracted from Coq into source code for the functional language OCaml together with calls to the Bulk Synchronous Parallel ML (BSML) library. In this paper we present a new core version of SyDPaCC for the development of parallel programs correct-by-contruction using the theory of list homomorphisms and algorithmic skeletons implemented and verified in Coq. The framework is illustrated on the the maximum prefix sum problem.
Type de document :
Article dans une revue
International Journal of Parallel Programming, Springer Verlag, 2017, 45 (2), pp.300-319. 〈10.1007/s10766-016-0415-8〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01159182
Contributeur : Frédéric Loulergue <>
Soumis le : mardi 8 mars 2016 - 12:00:28
Dernière modification le : jeudi 15 juin 2017 - 09:09:10
Document(s) archivé(s) le : dimanche 13 novembre 2016 - 10:42:22

Fichier

article.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Copyright (Tous droits réservés)

Identifiants

Collections

Citation

Frédéric Loulergue, Wadoud Bousdira, Julien Tesson. Calculating Parallel Programs in Coq using List Homomorphisms. International Journal of Parallel Programming, Springer Verlag, 2017, 45 (2), pp.300-319. 〈10.1007/s10766-016-0415-8〉. 〈hal-01159182〉

Partager

Métriques

Consultations de la notice

386

Téléchargements de fichiers

158