Skip to Main content Skip to Navigation
Conference papers

A Verified Accumulate Algorithmic Skeleton

Abstract : This paper presents an extension of a library for the Coq interactive theorem prover that enables the development of correct functional parallel programs based on sequential program transformation and automatic parallelization using an algorithmic skeleton named accumulate. Such an algorithmic skeleton is a pattern of a parallel algorithm that is provided as a high-order function implemented in parallel. The use of this framework is illustrated with the bracket matching problem, including experiments on a parallel machine.
Document type :
Conference papers
Complete list of metadata
Contributor : Frédéric Loulergue Connect in order to contact the contributor
Submitted on : Tuesday, October 15, 2019 - 6:39:35 PM
Last modification on : Tuesday, January 18, 2022 - 5:44:01 PM



Frédéric Loulergue. A Verified Accumulate Algorithmic Skeleton. 2017 Fifth International Symposium on Computing and Networking (CANDAR), Nov 2017, Aomori, France. pp.420-426, ⟨10.1109/CANDAR.2017.108⟩. ⟨hal-02317096⟩



Record views