package coq-coqeal

  1. Overview
  2. No Docs
CoqEAL - The Coq Effective Algebra Library

Install

Dune Dependency

github.com Edit opam file Versions (15)

Authors

  1. G
    Guillaume Cano
  2. C
    Cyril Cohen
  3. M
    Maxime Dénès
  4. A
    Anders Mörtberg
  5. V
    Vincent Siles

Maintainers

  1. C
    Cyril Cohen <cyril.cohen@inria.fr>

Sources

1.0.1.tar.gz
sha512=e41a97f89aca2ac18cffdf5795e16b60b44eac4e46512e4f5779ce49e2edff6d66b5ab89dd21e9255ba2facde4925e2ddf5e6bd594aea4a427f0916711e09f75

Description

This Coq library contains a subset of the work that was developed in the context of the ForMath EU FP7 project (2009-2013). It has two parts:

  • theory, which contains developments in algebra and optimized algorithms on mathcomp data structures.
  • refinements, which is a framework to ease change of data representations during a proof.

Tags

category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keyword:effective algebra keyword:elementary divisor rings keyword:Smith normal form keyword:mathematical components keyword:Bareiss keyword:Karatsuba multiplication keyword:refinements logpath:CoqEAL

Published: 18 Nov 2019

Dependencies (5)

  1. coq-mathcomp-algebra (>= "1.8.0" & < "1.10~")
  2. coq-mathcomp-multinomials (>= "1.2" & < "1.4~")
  3. coq-paramcoq (>= "1.1.1")
  4. coq-bignums (>= "8.7" & < "8.12~")
  5. coq (>= "8.7" & < "8.12~")

Dev Dependencies

None

Used by (1)

  1. coq-validsdp < "1.0.0"

Conflicts

None