Calculating Parallel Programs in Coq Using List Homomorphisms
Calculating Parallel Programs in Coq Using List Homomorphisms
复制标题
使用列表同态计算 Coq 中的并行程序
DOI：
10.1007/s10766-016-0415-8
复制
发表时间：
2016
影响因子：
1.5
通讯作者：
J. Tesson
中科院分区：
文献类型：
--
作者：
F. Loulergue;Wadoud Bousdira;J. Tesson
SyDPaCC是Coq验证助手的一组库。它允许编写被认为是规范的原始函数式程序（即具有高复杂性的程序），并将它们转换为更有效的版本。这些更高效的版本可以自动并行化，然后从Coq中提取到函数式语言OCaml的源代码中，同时调用批量同步并行ML库。在本文中，我们提出了一个新的SyDPaCC核心版本，用于使用列表同态理论和算法骨架开发并行程序，并在Coq中实现和验证。给出了最大前缀和问题的框架。
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.