Paper Info
Title
Formal derivation and extraction of a parallel program for the all nearest smaller values problem
Abstract
The All Nearest Smaller Values (ANSV) problem is an important problem for parallel programming as it can be used to solve several problems and is one of the phases of several other parallel algorithms. We formally develop by construction a functional parallel program for solving the ANSV problem using the theory of Bulk Synchronous Parallel (BSP) homomorphisms within the Coq proof assistant. The performances of the Bulk Synchronous Parallel ML program obtained from Coq is compared to a version derived without software support (pen-and-paper) and implemented using the Orléans Skeleton Library of algorithmic skeletons, and to a (unproved correct) direct implementation of the BSP algorithm of He and Huang.
Year
DOI
Venue
2014
10.1145/2554850.2554912
SAC
Keywords
Field
DocType
algorithms,coq proof assistant,specifying and verifying and reasoning about programs,parallel programming,functional parallel programming,algorithmic skeletons,verification,applicative programming,constructive algorithmics,all nearest smaller values problem,performance
Parallel algorithm,Computer science,Algorithmic skeleton,Algorithm,Software,Homomorphism,Bulk synchronous parallel,Proof assistant
Conference
Citations 
PageRank 
References 
2
0.37
19
Authors
5
Name
Order
Citations
PageRank
Frédéric Loulergue122336.83
Simon Robillard252.13
Julien Tesson3334.49
Joeffrey Legaux4203.13
Zhenjiang Hu5134199.25