| 10 | | * [S05] Definition of New Nestable Algorithmic Skeletons |
| 11 | | * [P06] Research report about "Definition of new algorithmic skeletons" |
| 12 | | * [S07] Proof of Algorithmic Skeletons |
| 13 | | * [P08] Research report about "Proving algorithmic skeletons in Coq" |
| 14 | | * [S09] Coq library for deriving parallel programs with algorithmic skeletons |
| 15 | | * [P10] Research report about "Derivation of parallel programs in Coq" |
| 16 | | * [S11] Some example applications with current definition of skeletons |
| 17 | | * [S12] Further example applications with full set of algorithmic skeletons |
| 18 | | * [P13] Research report about "Example applications developed with algorithmic skeletons and their derivation from specification" |
| | 14 | * [S05*] Functional Models of !MapReduce (software) |
| | 15 | * [P06*] Skeletal Parallelism on Top of !MapReduce ([http://frederic.loulergue.eu/ftp/papdas_p06.pdf report]) |
| | 16 | * [S07*] A Verified GTA Library in Coq ([http://frederic.loulergue.eu/ftp/SyDPaCC-ITP2014.tar.bz2 software]) |
| | 17 | * [P08*] A Verified GTA Coq Library for Parallel Program Extraction ([http://frederic.loulergue.eu/ftp/papdas_p08.pdf report]) |
| | 18 | * [S09*] Powerlists in Coq ([https://traclifo.univ-orleans.fr/SDPP/raw-attachment/wiki/PowerLists/PowerlistInCoq-0.1alpha.tar.gz software]) |
| | 19 | * [P10*] Parallel Program Development with Powerlists ([http://frederic.loulergue.eu/ftp/papdas_p10.pdf report]) |
| | 20 | * [S11*] SyDPaCC: Calculating Parallel Programs in Coq with BSP Homomorphisms ([http://frederic.loulergue.eu/ftp/SDPP-nii2013.tar.bz2 software]) |
| | 21 | * [S12*] SyDPaCC: Calculating Parallel Programs in Coq with BSP Homomorphisms ([http://frederic.loulergue.eu/ftp/sydpacc-core-0.2pre.tar.gz software]) |
| | 22 | * [P13*] Calculating Parallel Programs in Coq with BSP and List Homomorphisms ([http://frederic.loulergue.eu/ftp/papdas_p13.pdf report] |
| 22 | | * '''[S14]''' Release of the !SkeTo Library version 1.5: [http://sketo.ipl-lab.org/archives/sketo-1.50pre.tar.gz SkeTo 1.5pre] |
| 23 | | * [S15] Release of the OSL Library version 1.0 |
| 24 | | * [P16] Report “Efficient C++ Meta-Programmed Algorithmic Skeleton Libraries” |
| 25 | | * [S17] Release of the !SkeTo Library version 2.0 |
| 26 | | * [S18] Release of the OSL Library version 1.5 |
| 27 | | * [P19] Report “Hybrid Parallelism in C++ Algorithmic Skeleton Libraries” |
| 28 | | * [S20] Release of a set of example skeletal applications |
| 29 | | * '''[P21]''' Report “[http://frederic.loulergue.eu/ftp/deliverable_p21.pdf Efficient Parallel Programming with BSP Homomorphisms]” |
| 30 | | * '''[S22]''' A Formal Semantics for !SkeTo and OSL in Coq: [http://frederic.loulergue.eu/ftp/OSLSemantics-0.1.tar.bz2 v0.1], [http://frederic.loulergue.eu/ftp/OSLSemantics-0.2.tar.bz2 v0.2] |
| 31 | | * '''[P23]''' Report "[http://frederic.loulergue.eu/ftp/deliverable_p23.pdf Mechanised Semantics of an Algorithmic Skeleton Library]" |
| 32 | | * '''[S24]''' A Verified Library of Algorithmic Skeletons: [http://frederic.loulergue.eu/ftp/OSLPrototype-0.1.tar.gz v0.1] |
| 33 | | * '''[P25]''' Report "[http://frederic.loulergue.eu/ftp/deliverable_p25.pdf A Verified Library of Algorithmic Skeletons]" |
| | 26 | * [S14+S17+S20] Release of the !SkeTo Library ([http://sketo.ipl-lab.org/archives/sketo-1.50pre.tar.gz software]) |
| | 27 | * [S15+S18+S20] Release of the OSL Library ([http://frederic.loulergue.eu/ftp/osl-0.1pre.tar.gz software]) |
| | 28 | * [P16] Efficient C++ Meta-Programmed Algorithmic Skeleton Libraries ([http://frederic.loulergue.eu/ftp/papdas_p16.pdf report]) |
| | 29 | * [P19*] Expressive C++ Algorithmic Skeleton Libraries ([http://frederic.loulergue.eu/ftp/papdas_p19.pdf report]) |
| | 30 | * [P21] Efficient Parallel Programming with BSP Homomorphisms ([http://frederic.loulergue.eu/ftp/papdas_p21.pdf report]) |
| | 31 | * [S22] A Formal Semantics for !SkeTo and OSL in Coq ([http://frederic.loulergue.eu/ftp/OSLSemantics-0.2.tar.bz2 software]) |
| | 32 | * [P23] A Formal Semantics for !SkeTo and OSL in Coq ([http://frederic.loulergue.eu/ftp/papdas_p23.pdf report]) |
| | 33 | * [S24*] A Verified Library of Algorithmic Skeletons in Coq ([http://frederic.loulergue.eu/ftp/OSLPrototype-0.1.tar.gz software]) |
| | 34 | * [P25*] A Verified Library of Algorithmic Skeletons ([http://frederic.loulergue.eu/ftp/papdas_p25.pdf report]) |
| 37 | | * [P26] Report “Definition and mechanization of ASC semantics” |
| 38 | | * [P27] Report “Extraction of skeleton based specifications” |
| 39 | | * [S28] Coq code for ASC and tool for extraction of ASC programs |
| 40 | | * ''[S29] Cancelled'' |
| 41 | | * ''[P30] Cancelled'' |
| 42 | | * [P31] Report "Mechanized distributed semantics of C-light+TCP/IP" |
| 43 | | * [P32] Report “Compiling ASC into C-light+TCP/IP” |
| 44 | | * [S33] !CompCert x86-TCP/IP |
| 45 | | * [P34] Report "!CompCert x86-TCP/IP" |
| 46 | | * [P35] Report "Mechanized semantics of C-light-MT" |
| 47 | | * [P36] Report "Compiling ASC into C-light-MT" |
| 48 | | * [S37] !CompCert x86MT |
| 49 | | * [P38] Report "!CompCert x86MT" |
| | 38 | * [P26*] Nested Atomic Sections with Thread Escape: A Formal Definition ([http://frederic.loulergue.eu/ftp/papdas_p26.pdf report]) |
| | 39 | * [P27*] Nested Atomic Sections with Thread Escape: Operational Semantics ([http://frederic.loulergue.eu/ftp/papdas_p27.pdf report]) |
| | 40 | * [S28*] !TransactionsInCoq ([https://traclifo.univ-orleans.fr/PaPDAS/raw-attachment/wiki/TransactionsInCoq/TransactionsInCoq-0.1beta.tar.gz software]) |
| | 41 | * [P36*] Nested Atomic Sections with Thread Escape: Operational Semantics ([http://frederic.loulergue.eu/ftp/papdas_p36.pdf report]) |
| | 42 | * [S37] ModularCompCertTSO (software) |
| | 43 | * [P38] ModularCompCertTSO (report) |
| | 44 | * [S29], [P30], [P31], [P32], [S33], [P34], [P35]: cancelled |
| | 45 | |
| | 46 | |
| | 47 | '* modified with respect to the initial plan. |
