= 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 ([http://www.info.kochi-tech.ac.jp/~kmatsu/MRModel/MRModel.lhs software])
 * [P06*] Skeletal Parallelism on Top of !MapReduce ([http://frederic.loulergue.eu/ftp/papdas_p06.pdf report])
 * [S07*] A Verified GTA Library in Coq ([http://frederic.loulergue.eu/ftp/SyDPaCC-ITP2014.tar.bz2 software])
 * [P08*] A Verified GTA Coq Library for Parallel Program Extraction ([http://frederic.loulergue.eu/ftp/papdas_p08.pdf report])
 * [S09*] Powerlists in Coq ([https://traclifo.univ-orleans.fr/SDPP/raw-attachment/wiki/PowerLists/PowerlistInCoq-0.1alpha.tar.gz software])
 * [P10*] Parallel Program Development with Powerlists ([http://frederic.loulergue.eu/ftp/papdas_p10.pdf report])
 * [S11*] SyDPaCC: Calculating Parallel Programs in Coq with BSP Homomorphisms ([http://frederic.loulergue.eu/ftp/SDPP-nii2013.tar.bz2 software])
 * [S12*] SyDPaCC: Calculating Parallel Programs in Coq with BSP Homomorphisms ([http://frederic.loulergue.eu/ftp/sydpacc-core-0.2pre.tar.gz software])
 * [P13*] Calculating Parallel Programs in Coq with BSP and List Homomorphisms ([http://frederic.loulergue.eu/ftp/papdas_p13.pdf report])

=== Task 2 ===

 * [S14+S17+S20] Release of the !SkeTo Library ([http://sketo.ipl-lab.org/archives/sketo-1.50pre.tar.gz software])
 * [S15+S18+S20] Release of the OSL Library ([http://frederic.loulergue.eu/ftp/osl-1.0pre.tar.bz2 software])
 * [P16] Efficient C++ Meta-Programmed Algorithmic Skeleton Libraries ([http://frederic.loulergue.eu/ftp/papdas_p16.pdf report])
 * [P19*] Expressive C++ Algorithmic Skeleton Libraries ([http://frederic.loulergue.eu/ftp/papdas_p19.pdf report])
 * [P21] Efficient Parallel Programming with BSP Homomorphisms ([http://frederic.loulergue.eu/ftp/papdas_p21.pdf report])
 * [S22] A Formal Semantics for !SkeTo and OSL in Coq ([http://frederic.loulergue.eu/ftp/OSLSemantics-0.2.tar.bz2 software])
 * [P23] A Formal Semantics for !SkeTo and OSL in Coq ([http://frederic.loulergue.eu/ftp/papdas_p23.pdf report])
 * [S24*] A Verified Library of Algorithmic Skeletons in Coq ([http://frederic.loulergue.eu/ftp/OSLPrototype-0.1.tar.gz software]) 
 * [P25*] A Verified Library of Algorithmic Skeletons ([http://frederic.loulergue.eu/ftp/papdas_p25.pdf report])

=== Task 3 ===

 * [P26*] Nested Atomic Sections with Thread Escape: A Formal Definition ([http://frederic.loulergue.eu/ftp/papdas_p26.pdf report])
 * [P27*] Nested Atomic Sections with Thread Escape: Operational Semantics ([http://frederic.loulergue.eu/ftp/papdas_p27.pdf report])	
 * [S28*] !TransactionsInCoq ([https://traclifo.univ-orleans.fr/PaPDAS/raw-attachment/wiki/TransactionsInCoq/TransactionsInCoq-0.1beta.tar.gz software])
 * [P36*] Nested Atomic Sections with Thread Escape: Compilation ([http://frederic.loulergue.eu/ftp/papdas_p36.pdf report])
 * [S29], [P30], [P31], [P32], [S33], [P34], [P35], [S37], [P38]: cancelled


'* modified with respect to the initial plan.