wiki:Deliverables

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