package coq-coqeal

You can search for identifiers within the package.

in-package search v0.2.0

CoqEAL - The Coq Effective Algebra Library

Install

Dune Dependency

github.com Edit opam file Versions (18)

Authors

Maintainers

C

Cyril Cohen <cyril.cohen@inria.fr>

Sources

sha512=25ddb07c349379b1ac01ff8483ad75bee4016ebd38783aeb4feb8ff9801485ec6fb190b0c8803c9b9486c060917660592f768c3b83a0d4dc51907745ccb7172a

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: 24 Jul 2026

Dependencies (7)

coq-mathcomp-real-closed >= "2.0.3"
coq-mathcomp-multinomials >= "2.4"
coq-mathcomp-algebra
coq-mathcomp-ssreflect >= "2.5" & < "2.7~"
coq-hierarchy-builder >= "1.9.0"
coq-elpi >= "2.5.0"
coq-bignums

Dev Dependencies (1)

coq (>= "9.0" & < "9.3~") | (= "dev")

Used by (4)

Conflicts

None

On This Page

Description
Dependencies (7)
Dev Dependencies (1)
Used by (4)
Conflicts