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.
Last modified 3 years ago
Last modified on Jul 17, 2015, 5:10:49 PM