package coq-bedrock2

  1. Overview
  2. No Docs
A work-in-progress language and compiler for verified low-level programming

Install

Dune Dependency

github.com Edit opam file Versions (8)

Authors

  1. M
    Massachusetts Institute of Technology
  2. K
    Kevix
  3. S
    SiFive

Maintainers

  1. J
    Jason Gross <jgross@mit.edu>

Sources

v0.0.5.tar.gz
sha512=a4101b4a526dd691fcce8e5d86c16001736c465d4bccbf2e913b4f17b4ee24fe4d51731955480d4b69e04823dda860388994eff2ccc087d046ef15e4ef429b72

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.

Tags

logpath:bedrock2

Published: 03 Apr 2023

Dependencies (4)

  1. zarith >= "1.11"
  2. coq-coqutil = "0.0.3"
  3. coq >= "8.15~"
  4. conf-findutils build

Dev Dependencies (1)

  1. conf-python-3 build & with-test

Used by (2)

  1. coq-bedrock2-compiler = "0.0.5"
  2. coq-rupicola = "0.0.7"

Conflicts

None