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

DOI10.1007/978-3-319-08970-6_17zbMath1416.68161OpenAlexW150943050MaRDI QIDQ2879257

Kento Emoto, Julien Tesson, Frédéric Loulergue

Publication date: 8 September 2014

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-08970-6_17

zbMATH Keywords

functional programmingCoqlist homomorphismsemiring computationbulk synchronous parallelismautomatic program calculation

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Functional programming and lambda calculus (68N18)

Related Items (1)

Recursion schemes in Coq

Uses Software

• Unnamed Item
• SyDPaCC

This page was built for publication: A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction