package rocq-linux-process-semantics-examples

You can search for identifiers within the package.

in-package search v0.2.0

Example proofs for rocq-linux-process-semantics

Install

Dune Dependency

github.com Edit opam file Versions (1)

Authors

T

Tej Chajed

Maintainers

J

Jason Gross <jason@theorem.dev>

Sources

v0.0.1.tar.gz

sha512=0a65fb0f09273fa642f33a87e978b5ddb8748013f34edd45c67a9f33b8d1c2313d9d15ee019332f378c43fe79eff47a2343fec87f9a441e770bd1f7737c01c0b

Description

The Rocq theory LinuxProcessSemantics.Examples: a complete proof that two small RISC-V Linux binaries (a C build and a Zig build of the same program) are observably equivalent, and worked instances of the patch-classifier and input-measure statements.

Published: 24 Oct 2026

Dependencies (8)

rocq-linux-process-semantics-common = version
rocq-linux-process-semantics-core = version
rocq-read-file >= "0.0.2"
coq-flocq >= "4.2"
rocq-stdpp >= "1.13.0"
rocq-stdlib >= "9.0"
rocq-core >= "9.2"
dune >= "3.23"

Dev Dependencies

None

Used by (1)

rocq-linux-process-semantics

Conflicts

None

On This Page

Description
Dependencies (8)
Dev Dependencies
Used by (1)
Conflicts