##### My 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/SDPP

## Students

**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)