Changes between Version 11 and Version 12 of FraDeCoPP-3


Ignore:
Timestamp:
Oct 7, 2013, 8:48:15 AM (5 years ago)
Author:
frederic.loulergue@…
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • FraDeCoPP-3

    v11 v12  
    1313* 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. 
    1414 
    15 * 11h15-12h00 Frédéric Loulergue (Université d'Orléans) , '''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. 
     15* 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. 
    1616 
    1717* 12h00-14h00 '''Déjeuner / Lunch (Restaurant l'Agora)'''