Changes between Version 14 and Version 15 of JINO-2


Ignore:
Timestamp:
Jan 18, 2013, 5:39:48 PM (5 years ago)
Author:
frederic.loulergue@…
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • JINO-2

    v14 v15  
    2525* 14h00-15h00 Zhenjiang Hu (National Institute for Informatics, Tokyo, Japan), '''A GTA Library for Systematic Parallel Programming with !MapReduce'''[[BR]]!MapReduce, being inspired by the map and reduce primitives available in many functional languages, is the de facto standard for large scale data-intensive parallel programming.  Although it has succeeded in popularizing the use of the two primitives for hiding the details of parallel computation, little effort has been made to emphasize the programming methodology behind, which has been intensively studied in the functional programming and program calculation fields. In this talk, I'd show that !MapReduce can be equipped with a programming theory in calculational form. By integrating the generate-and-test programing (GTA) paradigm and semirings for aggregation of results, we propose a novel parallel programming framework for !MapReduce, and demonstrate how the framework can be efficiently implemented as a library to support parallel programming on Hadoop.[[BR]]This is a joint work with Kento Emoto, Sebastian Fischer, and Yu Liu. 
    2626 
    27 * 15h00-15h45  Frédéric Loulergue (LIFO, Université d'Orléans), '''Towards a Verified GTA Library in Coq'''[[BR]]The goal of this work is threefold. First we aim at modelling the algebraic structures used in the GTA framework and prove the lemma used to calculate programs from their GTA from inside the Coq proof assistant. Second we aim at providing some automation inside Coq to ease the definition of applications, with the formal verification that they actually fullfill the requirements of the GTA framework. Third we aim at providing the way to extract automatically actual parallel functional programs and MapReduce programs from these Coq developments. This talk will present the current status of this work-in-progress.[[BR]]This is a joint work with Kento Emoto, Julien Tesson, and Frédéric Dabrowski. 
     27* 15h00-15h45  Frédéric Loulergue (LIFO, Université d'Orléans), '''Towards a Verified GTA Library in Coq'''[[BR]]The goal of this work is threefold. First we aim at modelling the algebraic structures used in the GTA framework and prove the lemma used to calculate programs from their GTA from inside the Coq proof assistant. Second we aim at providing some automation inside Coq to ease the definition of applications, with the formal verification that they actually fullfill the requirements of the GTA framework. Third we aim at providing the way to extract automatically actual parallel functional programs and !MapReduce programs from these Coq developments. This talk will present the current status of this work-in-progress.[[BR]]This is a joint work with Kento Emoto, Julien Tesson, and Frédéric Dabrowski. 
    2828 
    2929* 15h45-16h15 '''Pause''' / '''Coffee Break'''