Version FrançaiseMy research interests in one sentence
I am interested in enhancing and pushing forward formal methods to ease the development of correct parallel programs.My research interests in few keywords
parallel 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 programs
I 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 development
I 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/SDPPStudents
- Former PhD students:
- Dr Victor Allombert (co-supervised with Frédéric Gava )
- Former Master students:
- Imane Rahmoun (co-supervised with Frédéric Gava)
Program Committee
International Workshop "Practical Aspects of High-Level Parallel Programming" (PAPP 2012, 2016 and 2017)
International Symposium on "High Level Parallel Programming and Applications" (2015)
International Workshop "Interaction and Concurrency Experience" (ICE) (2016)