Deliverables of the PaPDAS Project

Organization (not publically available)

• [R01] Roadmap of the project
• [R02] 6 months report
• [R03] 18 months report
• [R04] Final report

Task 1

• [S05*] Functional Models of MapReduce (​software)
• [P06*] Skeletal Parallelism on Top of MapReduce (​report)
• [S07*] A Verified GTA Library in Coq (​software)
• [P08*] A Verified GTA Coq Library for Parallel Program Extraction (​report)
• [S09*] Powerlists in Coq (​software)
• [P10*] Parallel Program Development with Powerlists (​report)
• [S11*] SyDPaCC: Calculating Parallel Programs in Coq with BSP Homomorphisms (​software)
• [S12*] SyDPaCC: Calculating Parallel Programs in Coq with BSP Homomorphisms (​software)
• [P13*] Calculating Parallel Programs in Coq with BSP and List Homomorphisms (​report)

Task 2

• [S14+S17+S20] Release of the SkeTo Library (​software)
• [S15+S18+S20] Release of the OSL Library (​software)
• [P16] Efficient C++ Meta-Programmed Algorithmic Skeleton Libraries (​report)
• [P19*] Expressive C++ Algorithmic Skeleton Libraries (​report)
• [P21] Efficient Parallel Programming with BSP Homomorphisms (​report)
• [S22] A Formal Semantics for SkeTo and OSL in Coq (​software)
• [P23] A Formal Semantics for SkeTo and OSL in Coq (​report)
• [S24*] A Verified Library of Algorithmic Skeletons in Coq (​software)
• [P25*] A Verified Library of Algorithmic Skeletons (​report)

Task 3

• [P26*] Nested Atomic Sections with Thread Escape: A Formal Definition (​report)
• [P27*] Nested Atomic Sections with Thread Escape: Operational Semantics (​report)
• [S28*] TransactionsInCoq (​software)
• [P36*] Nested Atomic Sections with Thread Escape: Compilation (​report)
• [S29], [P30], [P31], [P32], [S33], [P34], [P35], [S37], [P38]: cancelled

'* modified with respect to the initial plan.