package coq-vcfloat

  1. Overview
  2. No Docs
VCFloat: Floating Point Round-off Error Analysis

Install

Dune Dependency

verinum.org Edit opam file Versions (3)

Authors

  1. A
    Andrew W. Appel
  2. A
    Ariel E. Kellison
  3. T
    Tahina Ramananandro
  4. P
    Paul Mountcastle
  5. B
    Benoit Meister
  6. R
    Richard Lethin

Maintainers

  1. A
    Andrew W. Appel <appel@princeton.edu>

Sources

v2.1.1.tar.gz
sha256=cd0098a7448e13116f4bb1faa3d93c6f1a8b5a6fa83be979875b432aeb9eb27e

Description

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

Tags

date:2023-08-31 keyword:decision procedure keyword:floating-point arithmetic category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VCFloat

Published: 31 Aug 2023

Dependencies (5)

  1. coq-bignums
  2. coq-compcert >= "3.12"
  3. coq-interval >= "4.8.0" & < "4.10~"
  4. coq-flocq >= "4.1.1" & < "5.0"
  5. coq >= "8.16" & < "8.18~"

Dev Dependencies

None

Used by (1)

  1. coq-vst-lib < "2.14"

Conflicts

None