Skip to Main content Skip to Navigation
New interface
Conference papers

A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction

Kento Emoto Frédéric Loulergue 1, * Julien Tesson 2 
* Corresponding author
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans
Abstract : The integration of the generate-and-test paradigm and semi-rings for the aggregation of results provides a parallel programming framework for large scale data-intensive applications. The so-called GTA framework allows a user to define an inefficient specification of his/her problem as a composition of a generator of all the candidate solutions, a tester of valid solutions, and an aggregator to combine the solutions. Through two calculation theorems a GTA specification is transformed into a divide-and-conquer efficient program that can be implemented in parallel. In this paper we present a verified implementation of this framework in the Coq proof assistant: efficient bulk synchronous parallel functional programs can be extracted from naive GTA specifications. We show how to apply this framework on an example, including performance experiments on parallel machines.
Complete list of metadata
Contributor : Frédéric Loulergue Connect in order to contact the contributor
Submitted on : Monday, March 24, 2014 - 3:59:28 AM
Last modification on : Saturday, June 25, 2022 - 10:12:31 AM


  • HAL Id : hal-00964061, version 1



Kento Emoto, Frédéric Loulergue, Julien Tesson. A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. Interactive Theorem Proving, 2014, Vienna, Austria. ⟨hal-00964061⟩



Record views