FEEVER Software

The ANR FEEVER project has developed or contributed to the following software packages.

  • jsCoq is a new all-encompassing programming and editing environment for Coq, allowing literate Coq programming in a safe and intuitive manner; it has already been used to showcase our efforts to bridge the gap between certified software development and DSP, with a particular focus on Faust;
  • Mini Faust.v is a toy version of Faust, with its semantics and a small logic for reasoning about Faust programs, written in the Coq theorem prover language (see the companion paper, presented at the LAC'2015 conference, for more information); note that this version is geared towards "educational" purposes, so it is not usable with realistic Faust programs;
  • Faustine, an OCaml-based interpreter for Faust and its vector first extension proposal; version V1.0 can be downloaded here;
  • FaustLive, a new technology that allows seamless embedding of Faust code within LLVM-based projects; the binary version for OSX can be downloaded here;
  • Faust, the main software platform of the FEEVER project; check out the comprehensive Faust website for downloads.