package coq-bedrock2-compiler

  1. Overview
  2. Homepage
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.

Tags

logpath:bedrock2

Published: 03 Oct 2022

Dependencies (5)

  1. zarith >= "1.11"
  2. coq-riscv = "0.0.2"
  3. coq-bedrock2 = "0.0.2"
  4. coq >= "8.15~"
  5. conf-findutils build

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover