package coq-bedrock2
A work-in-progress language and compiler for verified low-level programming
Install
Dune Dependency
Authors
Maintainers
Sources
v0.0.9.tar.gz
sha512=6dec4778d54e4276aa81f1252759eb138dfe59ab413384b9a3729dc6c0b5f125aa80a23dc55770369c69f455c14388277e7f5bf3c88b141d8c493cd2d3de92a0
Description
bedrock2 is a low-level systems programming language. This language is equipped with a simple program logic for proving correctness of the programs. A verified compiler targeting RISC-V from this language exists in the coq-bedrock2-compiler package on opam.
The project has similar goals as bedrock, but uses a different design. No code is shared between bedrock and bedrock2.
Dependencies (4)
-
zarith
>= "1.11" -
coq-coqutil
= "0.0.7" -
coq
>= "9.0~" -
conf-findutils
build
Dev Dependencies (1)
-
conf-python-3
build & with-test
Used by (2)
-
coq-bedrock2-compiler
>= "0.0.9" -
coq-rupicola
>= "0.0.11"
Conflicts
None
On This Page