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