package coq-addition-chains

  1. Overview
  2. No Docs
Exponentiation algorithms following addition chains in Coq

Install

Dune Dependency

github.com Edit opam file Versions (4)

Authors

  1. P
    Pierre Castéran
  2. Y
    Yves Bertot

Maintainers

  1. P
    palmskog@gmail.com

Sources

v0.9.tar.gz
sha512=d793c993b50dd1149475ed7131ddb7910a30b6711c97f3ae8079661e2e8f4211ce8b4d85ade9e57c176b05feb20edb59d286db883a5873e3c775aac0fb1e40c5

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.

Tags

category:Mathematics/Combinatorics and Graph Theory keyword:addition chains keyword:exponentiation algorithms logpath:additions date:2022-05-20

Published: 25 May 2022

Dependencies (5)

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

Dev Dependencies

None

Used by

None

Conflicts

None