Changes between Version 12 and Version 13 of FraDeCoPP-3


Ignore:
Timestamp:
Oct 7, 2013, 1:32:20 PM (5 years ago)
Author:
frederic.loulergue@…
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • FraDeCoPP-3

    v12 v13  
    1111* 10h20-10h30 '''Accueil et introduction / Welcome and Introduction''' 
    1212 
    13 * 10h30-11h15 Julien Tesson (Université Paris Est Créteil) and Joeffrey Legaux (Université d'Orléans), '''Programming with BSP Homomorphisms'''[[BR]]Algorithmic skeletons in conjunction with list homomorphisms play an important role in formal development of parallel algorithms. We have designed a notion of homomorphism dedicated to bulk synchronous parallelism. In this paper we derive two application using this theory: sparse matrix vector multiplication and the all nearest smaller values problem. We implement a support for BSP homomorphism in the Orléans Skeleton Library and experiment it with these two applications. 
     13* 10h30-11h15 Julien Tesson (Université Paris Est Créteil) and Joeffrey Legaux (Université d'Orléans), '''[http://frederic.loulergue.eu/ftp/tesson_fradecopp-3.pdf Programming with BSP Homomorphisms]'''[[BR]]Algorithmic skeletons in conjunction with list homomorphisms play an important role in formal development of parallel algorithms. We have designed a notion of homomorphism dedicated to bulk synchronous parallelism. In this paper we derive two application using this theory: sparse matrix vector multiplication and the all nearest smaller values problem. We implement a support for BSP homomorphism in the Orléans Skeleton Library and experiment it with these two applications. 
    1414 
    1515* 11h15-12h00 Frédéric Loulergue (Université d'Orléans) , '''[http://frederic.loulergue.eu/ftp/loulergue_fradecopp-3.pdf Parallel Programming in Coq: the Bulk Synchronous Parallel ML Case]'''[[BR]]Bulk Synchronous Parallel ML (BSML) is a structured parallel functional programming language. It extends a functional programming language of the ML family with a polymorphic data structure and a very small set of primitives. In this paper we describe a framework for reasoning about BSML programs using the Coq interactive theorem prover and for extracting actual parallel programs from proofs. This framework is illustrated through applications.