Active development
SyDPaCC is a set of libraries for the interactive theorem prover Coq. SyDPaCC can be used to write and prove the correctness of bulk synchronous parallel functional programs as well as to develop correct-by-construction parallel programs from functional specifications. It has been developed in cooperation with Université Paris-Est Créteil, Kyushu Institute of Technology and the National Institute of Informatics (Japan).
https://sydpacc.github.io
SaIL stands for SAfe Interactive Language. It aims at improving safety in Reactive Domain Specific Languages. The long term objectives are: safe, garbage collection free, memory handling with an ownership type system, efficient parallel scheduling of memory independent processes, program proof support.
https://github.com/sail-pl/SAIL
VRAC stands for Verified Runtime Assertion Checking. This is a work-in-progress set of C code generators from code mixing C and ACSL (ANSI/ISO C Specification Language). These generators are verified using the Coq proof assistant.
https://github.com/fredericloulergue/vrac
WhyBSML is a set of WhyML modules (the langage of Why3) that formalize the BSML primitives and that use this formalization to implement and verify parallel functions. Compilable OCaml and BSML code can be extracted from WhyBSML and run on parallel machines.
https://whybsml.github.io
BSML is a library for the functional language OCaml. It provides a set of primitives for programming bulk synchronous parallel programs, and a standard library implemented on top of these primitives. BSML thus provides and API for scalable parallel programming with predictable performances. BSML has been developed in cooperation with Université Paris-Est Créteil, since 2000.
https://bsml-lang.github.io
Other software
PySke is a Python library on top of MPI providing a set of data-parallel algorithmic skeletons implemented using program transformation at runtime for optimisation. It has been developed since 2018. This library is available to all Python developers in the Python Package Index.
https://pyske.github.io