package coq-vcfloat

You can search for identifiers within the package.

in-package search v0.2.0

VCFloat: Floating Point Round-off Error Analysis

Install

Dune Dependency

verinum.org Edit opam file Versions (7)

Authors

Maintainers

A

Andrew W. Appel <appel@princeton.edu>

Sources

sha256=b11903380b9cece655c72ba50818a58b4a57b1cb2db0bedda04a5238347e326b

Description

VCFloat is a tool for Coq proofs about floating-point round-off error.

Tags

date:2026-09-22 keyword:decision procedure keyword:floating-point arithmetic category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VCFloat

Published: 24 Sep 2026

Dependencies (6)

coq-bignums
coq-compcert >= "3.18"
coq-interval >= "4.11.5"
coq-flocq >= "4.1.4" & < "5.0"
rocq-stdlib
coq-core >= "9.0" & < "9.3~"

Dev Dependencies

None

Used by (3)

coq-vst >= "3.1beta"
coq-vst-lib != "2.13"
rocq-laproof

Conflicts

None

On This Page

Description
Dependencies (6)
Dev Dependencies
Used by (3)
Conflicts