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

DOI10.1007/978-3-319-08970-6_17MaRDI QIDQ2879257zbMATH OpenOpenAlexFDO

Authors Kento Emoto, Julien Tesson, F. 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

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

Recommendations

• A Coq library for verification of concurrent programs
• scientific article; zbMATH DE number 3890706
• Transforming generate-and-test programs to execute under committed-choice AND-parallelism
• A Coq library for internal verification of running-times
• Coquet: a Coq library for verifying hardware
• Synthesizing and verifying multicore parallelism in categories of nested code graphs
• Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves
• scientific article; zbMATH DE number 4119602

Cited in

(3)

• Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves
• Recursion schemes in Coq
• Verified scalable parallel computing with Why3

Describes a project that uses

Uses Software

• SyDPaCC
• Coq

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2879257)