package coq-addition-chains

  1. Overview
  2. Homepage
Exponentiation algorithms following addition chains in Coq

Install

Dune Dependency

Authors

Maintainers

Sources

v0.6.tar.gz
sha512=a7e5e16506ad4eb2b5968d6bffbc1dacb297a304c7e8bbbd2ec4d2488d2090573288bdcd0e17fa05b605925b71c3ece5e46e91134d98f47248ef173c92dc8ed7

Description

Addition chains are algorithms for computations of the p-th power of some x, with the least number of multiplications possible. This development provides a few implementations of addition chains in Coq, including proofs of their correctness.

Dependencies (5)

  1. coq-mathcomp-algebra
  2. coq-mathcomp-ssreflect >= "1.12.0" & < "1.15~"
  3. coq-paramcoq >= "1.1.3"
  4. coq >= "8.13" & < "8.16~"
  5. dune >= "2.5"

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover