search

coq-community / coqeal

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Other
66 stars 17 forks source link

Refinement of MathComp matrices and matrix operations #72

Open palmskog opened 1 year ago

palmskog commented 1 year ago

For doing computation inside Coq using matrices, the most efficient way is likely as operations on Coq's primitive arrays. However, to make the connection to abstract MathComp matrices, there needs to be a refinement from them down to primitive arrays of arrays (e.g., via the refinement to lists of lists).

Suggested by a problem faced by @spitters.

palmskog commented 1 year ago

Another project that looks at the problem of efficient matrix computation, and is now also licensed under the MIT license: https://github.com/zhengpushi/coq-matrix

Might be possible to integrate some of the approaches into CoqEAL.