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

vcfloat-2.2.tar.gz
sha256=5d57a3f0e69453460e729f26f00597e456a4ee2502f0886acf11d7908692af46

Description

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

Tags

date:2024-03-20 keyword:decision procedure keyword:floating-point arithmetic category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VCFloat

Published: 21 Mar 2024

Dependencies (5)

  1. coq-bignums
  2. coq-compcert >= "3.13"
  3. coq-interval >= "4.10.0"
  4. coq-flocq >= "4.1.4" & < "5.0"
  5. coq >= "8.19" & < "8.21~"

Dev Dependencies

None

Used by (1)

  1. coq-vst-lib != "2.13"

Conflicts

None