Rocq Elm Extraction

A framework for extracting Rocq programs to Elm.

Meta

• Author(s):
  • Danil Annenkov (initial)
  • Mikkel Milo (initial)
  • Jakob Botsch Nielsen (initial)
  • Bas Spitters (initial)
  • Eske Hoy Nielsen
• License: MIT
• Compatible Rocq versions: 9.0 or later
• Additional dependencies: MetaRocq
• Rocq namespace: ElmExtraction
• Related publication(s):
  • Extracting functional programs from Coq, in Coq doi:10.1017/S0956796822000077
  • "Extending MetaCoq Erasure: Extraction to Rust and Elm"
  • "Extracting Smart Contracts Tested and Verified in Coq" doi:10.1145/3437992.3439934

Building and installation instructions

The easiest way to install the latest released version is via OPAM:

opam repo add rocq-released https://rocq-prover.org/opam/released
opam install coq-elm-extraction

To instead build and install manually, do:

opam repo add rocq-released https://rocq-prover.org/opam/released
git clone https://github.com/AU-COBRA/coq-elm-extraction.git
cd coq-elm-extraction
opam install . --deps-only
make #or make -j <number-of-cores-on-your-machine>
make install

Documentation

For documentation see examples and generated RocqDoc.

Additional examples can be found in ConCert.