Changes between Version 12 and Version 13 of WikiStart
- Timestamp:
- Jul 15, 2014, 7:19:02 AM (4 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
WikiStart
v12 v13 23 23 == Software == 24 24 25 * ''' SyDPaCC''' [http://frederic.loulergue.eu/ftp/SyDPaCC-Jan2014.tar.bz2 version Jan2014](requires [http://traclifo.univ-orleans.fr/BSML BSML] for compiling parallel programs)25 * '''The SyDPaCC Framework''': [http://frederic.loulergue.eu/ftp/SyDPaCC-ITP2014.tar.bz2 version ITP2014], [http://frederic.loulergue.eu/ftp/SyDPaCC-Jan2014.tar.bz2 version Jan2014] (requires [http://traclifo.univ-orleans.fr/BSML BSML] for compiling parallel programs) 26 26 * Library "Systematic Development of Parallel Programs" [http://frederic.loulergue.eu/ftp/sdpp-0.1.tar.bz2 version 0.1], [http://frederic.loulergue.eu/ftp/SDPP-nii2013.tar.bz2 version nii2013] (includes CertifiedBSML version nii2013, !ProgramCalculationInCoq version 0.16, LIFO) 27 27 * Library "Program Calculation in Coq": [http://frederic.loulergue.eu/ftp/ProgramCalculationInCoq-0.1.tar.bz2 version 0.1], [http://frederic.loulergue.eu/ftp/ProgramCalculationInCoq-0.15.tar.bz2 version 0.15], [http://frederic.loulergue.eu/ftp/ProgramCalculationInCoq-0.16.tar.bz2 version 0.16] (for Coq 8.3), [https://traclifo.univ-orleans.fr/SDPP/raw-attachment/wiki/WikiStart/ProgramCalculationInCoq-nii2013.tar.gz version nii2013] (for Coq 8.4) … … 31 31 === Conferences === 32 32 33 * Kento Emoto, Frédéric Loulergue, and Julien Tesson. A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. In Interactive Theorem Proving (ITP), LNCS. Springer, 2014. to appear.33 * Kento Emoto, Frédéric Loulergue, and Julien Tesson. [http://dx.doi.org/10.1007/978-3-319-08970-6_17 A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction]. In ITP, number 8558 in LNAI, pages 258-274. Springer, 2014. [ DOI ] 34 34 * Frédéric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Legaux, and Zhenjiang Hu. Formal Derivation and Extraction of a Parallel Program for the All Nearest Smaller Values Problem. In ACM Symposium on Applied Computing (SAC), pages 1577-1584. ACM Press, 2014 35 35 * Frédéric Loulergue, Virginia Niculescu, and Simon Robillard. [http://dx.doi.org/10.1109/CANDAR.2013.17 Powerlists in Coq: Programming and Reasoning]. In First International Symposium on Computing and Networking (CANDAR), pages 57-65. IEEE Computer Society, 2013