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

Authors

Maintainers

A

Andrew W. Appel <appel@princeton.edu>

Sources

sha256=cfc2c132adda1d955d1ded3578c7c574d180064674de93e24e0e82e965a09f6e

Description

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

Tags

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

Published: 07 Apr 2026

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