An Agda backend to generate MetaCoq λ□ (LambdaBox) programs for further verified extraction to WASM or Rust using the Peregrine tool. The backend builds off Agda 2.7.0.1. Compatible with Coq 8.19.0, MetaCoq 1.3.1 and CertiCoq 0.9.
To install the backend, setup GHC (tested with 9.10.1) and cabal.
git clone git@github.com:agda/agda2lambox.git
cd agda2lambox
cabal install
agda2lambox [AGDAFLAGS] [--out-dir DIR] [--typed] [--no-blocks] FILE
Then, use the following tool to further compile the generated .ast files to WASM, Rust, OCaml, C, and Elm.
The backend generates .v and .txt files that contain the extracted λ□ environment.
To check what's generated, setup CertiCoq and compile the minimal Coq prelude.
opam pin add certicoq 0.9+8.19
coq_makefile -f _CoqProject -o CoqMakefile
make -f CoqMakefile
- Type aliases (See #3)
- Improve type compilation
- The (re)implementation of the type translation is currently incomplete. In particular, when compiling an application, we should retrieve the type of the head and compile the elims with it.
- Check support for Agda-specific edge cases
- Projection-like (See #6)
- Support primitives (ints and floats)
- Setup compilation to Wasm/Rust using Certicoq
- Setup proper testing infrastructure
Things that ought to be implemented, but not right now.
- Caching of compiled modules.
- The MetaCoq Project
- The CertiCoq Compilation pipeline
- CertiCoqWASM
- Pierre Letouzey's thesis introducing λ□ (in French)
- Verified Extraction from Coq to OCaml and its accompanying paper
- Certified Erasure for Coq, in Coq
- Extracting functional programs from Coq, in Coq
- Lambdabox syntax and untyped environments
- Lambdabox typed environments
- Coq Extraction Pipeline
- Extraction Example