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. Ã
    Érik Martin-Dorel
  5. A
    Anders Mörtberg
  6. D
    Damien Rouhling
  7. P
    Pierre Roux
  8. V
    Vincent Siles

Maintainers

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

Sources

1.1.2.tar.gz
sha512=7bba8d8c69b080a1eec3b39e61ff2b8ee1147b60f69cfa5398cd9030f098b95c3f4b4cc0a38c31d0b5d6d88648d6478b07dbe29d58c04e955df102a0afd86f4a

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 including normal forms of matrices, 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: 13 Mar 2023

Dependencies (3)

  1. coq-mathcomp-multinomials >= "1.5.1" & < "1.6~"
  2. coq-paramcoq >= "1.1.3"
  3. coq-bignums < "9~"

Dev Dependencies (3)

  1. coq-mathcomp-real-closed (>= "1.1.2" & < "1.2~") | (= "dev")
  2. coq-mathcomp-algebra ((>= "1.13.0" & < "1.17~") | = "dev")
  3. coq (>= "8.15" & < "8.18~") | (= "dev")

Conflicts

None