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 (5)

Authors

Maintainers

A

Andrew W. Appel <appel@princeton.edu>

Sources

sha256=8500c0bed5145e435be533eac8cc8dee594198d3006ba90a15e8a06706a13695

Description

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

Tags

date:2025-11-14 keyword:decision procedure keyword:floating-point arithmetic category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VCFloat

Published: 18 Nov 2025

Dependencies (5)

coq-bignums
coq-compcert >= "3.16"
coq-interval >= "4.10.0"
coq-flocq >= "4.1.4" & < "5.0"
coq >= "9.0" & < "9.2~"

Dev Dependencies

None

Used by (2)

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

Conflicts

None

On This Page

Description
Dependencies (5)
Dev Dependencies
Used by (2)
Conflicts