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

2.1.tar.gz
sha256=5ae06c6c2d3e341f8315442f3fe87e199be8e88255ac30620b85469212521faf

Description

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

Tags

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

Published: 14 Apr 2023

Dependencies (5)

  1. coq-bignums
  2. coq-compcert >= "3.11"
  3. coq-interval >= "4.5.2" & < "4.8.0"
  4. coq-flocq >= "4.1.0" & < "5.0"
  5. coq >= "8.16" & < "8.18~"

Dev Dependencies

None

Used by (1)

  1. coq-vst-lib < "2.14"

Conflicts

None