@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.