[isabelle] Polynomials over GF(2)

Greetings -

I am working on a formal development of an efficient software algorithm
to calculate a proprietary cyclic redundancy check (CRC). This CRC
itself is defined in the usual fashion in terms of polynomials over

Rather than re-invent the wheel, I'd like to re-use existing Isabelle
theories as much as possible.  I'm interested in theories in any of the
following areas:
  --  polynomials over a field
  --  GF(2)
  --  CRC specifications and algorithms

If anyone can point me towards such material, I would be grateful.
Thanks - Mark Janney

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.