other.bib

@phdthesis{TES2011:THESIS,
  author = {Tesson, Julien},
  title = {Environnement pour le d\'{e}veloppement et la preuve de correction 
                  syst\'{e}matiques de programmes parall\`{e}les fonctionnels},
  school = {LIFO, University of Orl\'{e}ans},
  year = 2011,
  month = {November},
  category = {t},
  url = {http://tel.archives-ouvertes.fr}
}
@phdthesis{JAV2011:THESIS,
  author = {Javed, Noman},
  title = {{Meta-programmed Algorithmic Skeletons: Implementations, Performances and Semantics}},
  school = {LIFO, University of Orl\'{e}ans},
  year = 2011,
  month = {October},
  category = {t},
  url = {http://tel.archives-ouvertes.fr}
}
@phdthesis{GES2009:THESIS,
  author = {Gesbert, L.},
  title = {{D\'eveloppement syst\'ematique et s\^uret\'e 
                   d'ex\'ecution en programmation parall\`ele structur\'ee}},
  school = {University Paris Est, LACL},
  year = 2009,
  category = {t},
  url = {http://tel.archives-ouvertes.fr/tel-00481376}
}
@mastersthesis{JAV2007:MASTER,
  author = {Javed, N.},
  title = {{An Efficient Bulk Synchronous Parallel Library of 
           Algorithmic Skeletons in C++}},
  school = {m\'emoire de Master, Universit\'e d'Orl\'eans, LIFO},
  year = 2007
}
@mastersthesis{TES2007:MASTER,
  author = {Tesson, J.},
  title = {{S\'emantique formelle de la biblioth\`eque BSPlib}},
  school = {m\'emoire de Master, Universit\'e d'Orl\'eans, LIFO},
  year = 2007
}
@mastersthesis{LRE2005:MASTER,
  author = {Louis-R\'egis, D.},
  title = {{Certification de programmes BSML 
                   avec juxtaposition parall\`ele}},
  school = {m\'emoire de Master, Universit\'e d'Orl\'eans, LIFO},
  year = 2005
}
@article{GAV2005:SCPE,
  author = {Gava, F.},
  title = {{External Memory in Bulk Synchronous Parallel ML}},
  journal = {Scalable Computing: Practice and Experience},
  year = 2005,
  volume = 6,
  number = 4,
  pages = {43-70},
  month = {December},
  category = {a},
  pdf = {http://www.pdcp.org/vols/vol06/no4/SCPE_6_4_04.pdf}
}
@phdthesis{GAV2005:THESIS,
  author = {Gava, F.},
  title = {{Approches fonctionnelles de la programmation parall\'ele et des m\'eta-ordinateurs. S\'emantiques, implantations et certification.}},
  school = {University Paris Val-de-Marne, LACL},
  year = 2005,
  category = {t}
}
@inproceedings{GAV2006:JFLA,
  author = {Gava, F.},
  title = {{Une implantation de la juxtaposition parall\`ele}},
  booktitle = {Journ\'ees Francophones des Langages Applicatifs (JFLA)},
  year = 2006,
  editor = {Moreau, P.-E. and Hardin, T.},
  organization = {INRIA},
  category = {e},
  teampdf = {../../ftp/gava_jfla2006.pdf}
}
@mastersthesis{BEL2005:MASTER,
  author = {Belbekkouche, A.},
  title = {{MSPML : Environnements de communication et tol\'erance aux pannes}},
  school = {University of Orl\'eans, LIFO},
  year = 2005,
  type = {Master Thesis},
  category = {t}
}
@mastersthesis{BEN2005:MASTER,
  author = {Benheddi, R.},
  title = {{Composition parall\`ele pour MSPML: s\'emantiques et implantation}},
  school = {University of Orl\'eans, LIFO},
  year = 2005,
  type = {Master Thesis},
  category = {t}
}
@inproceedings{GAV2005:HLPP,
  author = {Gava, F.},
  title = {{Implementation of Parallel Data Structures in BSML}},
  booktitle = {Third International Workshop on High-Level Parallel Programming and Applications (HLPP 2005)},
  pages = {161-174},
  year = 2005,
  editor = {Loulergue, F. and Tiskin, A.},
  month = {June},
  category = {}
}
@inproceedings{GAV2004:ICCSa,
  author = {Gava, F.},
  title = {{Parallel I/O in Bulk Synchronous Parallel ML}},
  booktitle = {The International Conference on Computational Science (ICCS 2004), Part III},
  year = 2004,
  editor = {Bubak, M. and van Albada, D. and  Sloot, P. and Dongarra, J.},
  series = {LNCS},
  publisher = {Springer Verlag},
  pages = {339-346},
  category = {c},
  abstract = {
    Bulk Synchronous Parallel ML or BSML is a functional data-parallel
    language for programming bulk synchronous parallel (BSP)
    algorithms. The execution time can be estimated and dead-locks and
    indeterminism are avoided. For large scale applications where
    parallel processing is helpful and where the total amount of data
    often exceeds the total main memory available, parallel disk I/O
    becomes a necessity. We present here a library of I/O features for
    BSML and its cost model.},
  teampdf = {papers/gava_iccs2004.pdf}
}
@inproceedings{GAV2004:ICCSb,
  author = {Gava, F.},
  title = {{Design of Deparmental Metacomputing ML}},
  booktitle = {The International Conference on Computational Science (ICCS 2004)},
  year = 2004,
  editor = {Bubak, M. and van Albada, D. and  Sloot, 
                  P. and Dongarra, J.},
  series = {LNCS},
  publisher = {Springer Verlag},
  pages = {50-53},
  category = {c},
  abstract = {
    Bulk Synchronous Parallel ML or BSML is a functional data-parallel
    language for programming bulk synchronous parallel (BSP)
    algorithms. The execution time can be estimated and dead-locks and
    indeterminism are avoided. For large scale applications, more than
    one parallel machine is needed. We consider here the design and
    cost-model of a BSML-like language devoted to the programming of
    such applications: Departmental Metacomputing ML or DMML.},
  teampdf = {papers/gava_iccs_papp2004.pdf}
}
@inproceedings{GAV2004:JFLA,
  author = {Gava, F.},
  title = {{Une biblioth\`eque certifi\'ee de programmes fonctionnels BSP}},
  booktitle = {Journ\'ees Francophones des Langages Applicatif, JFLA},
  year = 2004,
  editor = {{M\'enissier-Morain, V.}},
  month = {january},
  publisher = {INRIA},
  pages = {55-68},
  category = {e},
  abstract = {
  },
  teampdf = {papers/gava_jfla2004.pdf}
}
@article{GAV2003:PPL,
  author = {Gava, F.},
  title = {{Formal Proofs of Functional BSP Programs}},
  journal = {Parallel Processing Letters},
  year = 2003,
  volume = 13,
  number = 3,
  pages = {365-376},
  category = {a},
  abstract = {
   The Bulk Synchronous Parallel ML (BSML) is a functional language
   for BSP programming, a model of computing which allows parallel
   programs to be ported to a wide range of architectures. It is based
   on an extension of the ML language by parallel operations on a
   parallel data structure called parallel vector, which is given by
   intention. We present a new approach to certifying BSML programs in
   the context of type theory. Given a specification and a program, an
   incomplete proof of the specification (of which algorithmic
   contents corresponds to the given program) is built in the type
   theory, in which gaps would correspond to the proof
   obligation. This development demonstrates the usefulness of
   higher-order logic in the process of software certification of
   parallel applications. It also shows that the proof of rather
   complex parallel algorithms may be done with inductive types
   without great difficulty by using existing certified programs. This
   work has been implemented in the Coq Proof Assistant, applied on
   non-trivial examples and is the basis of a certified library of
   BSML programs.},
  teampdf = {papers/gava_ppl2003.pdf}
}
@mastersthesis{GAV2002:MASTER,
  author = {Fr\'ed\'eric Gava},
  title = {{A Polymorphic Type System for BSML}},
  school = {University Paris Val de Marne},
  year = {2002},
  teampdf = {http://f.loulergue.free.fr/ftp/TR-2002-12.pdf},
  category = {t},
  abstract = {
    The BSMLlib library is a library for Bulk Synchronous Parallel
    (BSP) programming with the functional language Objective Caml. It
    is based on an extension of the $\lambda$-calculus by parallel
    operations on a data structure named parallel vector, which is
    given by intention. In order to have an execution that follows the
    BSP model, and to have a simple cost model, nesting of parallel
    vectors is not allowed. The novelty of this work is a type system
    which prevents such nesting. This system is correct w.r.t.\ the
    dynamic semantics which is also presented. An inference algorithm
    is given.}
}
@mastersthesis{BIL2004:MASTER,
  author = {David Billiet},
  title = {{BSML: Impl\'ementation modulaire et pr\'evision de performances}},
  school = {University Paris Val de Marne},
  month = {september},
  year = {2004},
  teampdf = {http://f.loulergue.free.fr/ftp/billiet_master_thesis_2004.pdf},
  category = {t},
  abstract = {
    BSML (Bulk-Synchronous Parallel ML) et DMML (Departmental
    Metacomputing ML) sont deux extensions ML pour la programmation
    fonctionnelle d'algorithmes parallèles.

    C'est autour de ces extensions que mon stage fût ax\'e. Tout
    d'abord, mon travail \'etait d'enrichir les impl\'ementations
    propos\'ees par la BSMLlib. La pr\'evision de performance est un
    \'el\'ement important dans l'\'elaboration de programmes, il \'etait
    n\'ecessaire d'avoir un programme \'ecrit en BSML permettant d'obtenir
    les paramètres BSP de la machine parallèle. En plus de ces
    paramètres, le programme permet aussi d'obtenir la puissance de
    calcul de cette même machine. Enfin, une exp\'erimentation a mis en
    \'evidence cette pr\'evision de performance.}
}
@mastersthesis{DAB2003:MASTER,
  author = {Fr\'ed\'eric Dabrowski},
  title = {{Pattern Matching and Exceptions Handling for
                   Bulk Synchronous Parallel ML}},
  school = {University Paris Val de Marne},
  year = 2003,
  teampdf = {http://f.loulergue.free.fr/ftp/TR-2003-06.pdf},
  category = {t},
  abstract = {
      The BSML (Bulk Synchronous ML) language is a data-parallel
      functional language for programming BSP (Bulk Synchronous
      algorithms) algorithms in so-called direct mode. In a direct
      mode BSP algorithm, the physical structure of processes is made
      explicit. The execution time can then be estimated and
      dead-locks and indeterminism are avoided.  The BSMLlib library,
      the current implementation of the BSML language, permits, as an
      extension of Objective Caml, the use of the exceptions handling
      mechanism that comes with this language.  However, the
      interaction of Objective Caml exceptions with the
      BS$\lambda$-calculus (the theoretical model underlying the BSML
      language) has not yet been studied and yields some safety
      issues.  In particular, the use of collective synchronization
      operations needs the participation of all processes during the
      call to one of these operation, should the opposite occur,
      processes involved in this call are locked. The BSML language,
      without exceptions, ensures that all processes participate to
      such a call and thus that dead-locks are avoided (except for
      process failure). When one introduces Objective Caml exceptions,
      this safety property does not hold any more.  Thus it is needed
      to study a new semantics, suitable to exceptions handling, to
      recover this property. The present work introduces such a
      semantics in which the participation of all processes is ensured
      and dead-lock issues are avoided.  We will also introduce a
      semantics allowing the pattern-matching of BSML parallel
      vectors. This semantics has been studied in the framework of a
      previous work on exceptions handling which has not been retained
      here but its functionalities will be nethertheless add to the
      BSML language.}
}
@mastersthesis{GES2005:MASTER,
  author = {Louis Gesbert},
  title = {{An Application of Variable Abstraction with Freshness}},
  school = {The University of Manchester},
  year = 2005,
  category = {t}
}

This file was generated by bibtex2html 1.96.