Software

  • SyDPaCC https://sydpacc.github.io 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).
  • PySke https://pyske.github.iois 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.
  • BSML https://bsml-lang.github.io 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 has been developed in cooperation with Université Paris-Est Créteil, since 2000.