Calculating Parallel Programs in Coq Using List Homomorphisms |
| |
Authors: | Frédéric Loulergue Wadoud Bousdira Julien Tesson |
| |
Affiliation: | 1.Inria πr2, PPS, CNRS,Univ. Paris Diderot,Paris,France;2.Univ. Orléans,INSA Centre Val de Loire, LIFO EA 4022,Orléans,France;3.LACL, UPEC,Université Paris Est,Créteil,France |
| |
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 library. In this paper we present a new core version of SyDPaCC for the development of parallel programs correct-by-construction using the theory of list homomorphisms and algorithmic skeletons implemented and verified in Coq. The framework is illustrated on the maximum prefix sum problem. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|