My research interests in one sentenceI am interested in enhancing and pushing forward formal methods to ease the development of correct parallel programs.
My research interests in few keywordsparallel programming, language semantics, parallel programs verification, algorithmic skeletons, constructive algorithmics, program transformation, verified compiler, shallow and deep embedding of languages in proof assistant logic.
Development of Correct Functional BSP programsI am using the proof assistant Coq to develop correct BSML programs.
Such correct development is done by progressively transforming a functional specification into a program which use BSML parallel primitives or into an algorithmic skeleton for which we have a parallel implementation proved correct. Each transformation step is proved correct by the proof assistant using axiomatic description of BSML primitives semantics.
Coq developmentI developed an environment for program calculation and some lemmas and mechanisms to help specification to skeleton transformations. The code, papers and research reports can be found here: https://traclifo.univ-orleans.fr/SDPP
- Former PhD students:
- Former Master students:
- Imane Rahmoun (co-supervised with Frédéric Gava)
International Symposium on "High Level Parallel Programming and Applications" (2015)
International Workshop "Interaction and Concurrency Experience" (ICE) (2016)