package coq-bedrock2-compiler

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

Install

Dune Dependency

github.com Edit opam file Versions (7)

Authors

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

Maintainers

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

Sources

v0.0.7.tar.gz
sha512=42e264df702c65915635f3a3276d3c841de67b3999ebae9b8727dcaa94222f1832bb56b04025a2aa4eb752531e18dc7f2effe83c491d7d22e8da66ca17cbd182

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.

Tags

logpath:bedrock2

Published: 20 Mar 2024

Dependencies (5)

  1. zarith >= "1.11"
  2. coq-riscv = "0.0.5"
  3. coq-bedrock2 = version
  4. coq >= "8.18~"
  5. conf-findutils build

Dev Dependencies

None

Used by (1)

  1. coq-fiat-crypto = "0.1.2"

Conflicts

None