PROPAC : Certified Parallel Programming
The goals of this project is
to produce a programming environment in which certified parallel
programs can be written, proved and safely executed.
More technically, several subgoals will be studied to achieve the
overall goal of the project:
Proofs, using the Coq proof assistant, of programs written with the
functional parallel languages we developped.
Certification of the compilers for these languages, from source code
to bytecode for parallel virtual machines and the certification of
these virtual machines
Proofs of imperative bulk synchronous parallel programs first written
with a small dedicated language and then with an extension of C or
Automatic performance prediction of the programs written with these
French Ministry of Research, Young Researchers Program
Action's Web Page