package coq-bedrock2-compiler
A work-in-progress language and compiler for verified low-level programming (compiler part)
Install
Dune Dependency
Authors
Maintainers
Sources
v0.0.2.tar.gz
sha512=4f2b2975eb3ed26158b4cf2eb6f8b2eb27fc381e57da5b0be4eb275c3306d71542938cdf614108975bf24d985b6991b95cb1f681406b9f0759f214d4eb33b337
Description
bedrock2 is a low-level systems programming language. This language is equipped with a simple program logic for proving correctness of the programs. This package includes a verified compiler targeting RISC-V from this language.
The project has similar goals as bedrock, but uses a different design. No code is shared between bedrock and bedrock2.
Dependencies (5)
-
zarith
>= "1.11" -
coq-riscv
= "0.0.2" -
coq-bedrock2
= "0.0.2" -
coq
>= "8.15~" -
conf-findutils
build
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page