Coq Rust Extraction

A framework for extracting Coq programs to Rust.

Meta

• Author(s):
  • Danil Annenkov (initial)
  • Mikkel Milo (initial)
  • Jakob Botsch Nielsen (initial)
  • Bas Spitters (initial)
  • Eske Hoy Nielsen
• License: MIT
• Compatible Coq versions: 8.20 or later
• Additional dependencies: MetaCoq
• Coq namespace: RustExtraction
• 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 coq-released https://coq.inria.fr/opam/released
opam install coq-rust-extraction

To instead build and install manually, do:

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

Documentation

For documentation see examples and generated CoqDoc.

Additional examples can be found in ConCert.