CAS 707 ─ Formal Specification Techniques ─ Winter 2018

To make communication easier, start with the following common definition of Huffman trees:

type hTree 'a =
  | Leaf : leaf : 'a -> hTree 'a
  | Branch : left : hTree 'a -> right : hTree 'a -> hTree 'a

Implement at least decoding of (finite) bit streams implemented as lists of Booleans.

Explore implementing also encoding and tree construction.

Document the alternatives you consider and your design decisions.

Possibly explore also adding specifications and interesting/useful lemmas.

Again produce a listings-based LaTeX document and submit both LaTeX source (including your F* source) and PDF to subversion by Monday, Jan. 22, morning at 11 a.m..

Please include also questions and problems you encounter!